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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
r : ℝ
⊢ (if (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r then natDegree (minpoly K x)
    else 0) =
    Multiset.count r
      (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
        (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
have pos : ∀ (hr : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r),
  natDegree (minpoly K x) =
    Multiset.count r
      (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
        (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
Tactic: split_ifs with hr
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
r : ℝ
pos :
  ∀ (hr : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r),
    natDegree (minpoly K x) =
      Multiset.count r
        (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
          (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
⊢ (if (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r then natDegree (minpoly K x)
    else 0) =
    Multiset.count r
      (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
        (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
have neg : ∀ (hr : ¬(spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r),
  0 =
    Multiset.count r
      (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
        (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
Tactic: split_ifs with hr
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
r : ℝ
hr : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
s : ℝ
hs :
  Membership.mem (γ := Multiset ℝ)
    (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
    s
⊢ r = s
have obtain : ∀ (a : E)
  (ha :
    Membership.mem (γ := Multiset E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))) a)
  (has : (spectralMulAlgNorm K E : (a : E) → ℝ) a = s), r = s
Tactic: obtain ⟨a, ha, has⟩ := Multiset.mem_map.mp hs
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
r : ℝ
hr : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
s : ℝ
hs :
  Membership.mem (γ := Multiset ℝ)
    (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
    s
a : E
ha :
  Membership.mem (γ := Multiset E)
    (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))) a
has : (spectralMulAlgNorm K E : (a : E) → ℝ) a = s
⊢ r = s
have rw : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = s
Tactic: rw [← hr, ← has, spectralMulAlgNorm_eq_of_mem_roots K L x ha]
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
r : ℝ
hr : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
s : ℝ
hs :
  Membership.mem (γ := Multiset ℝ)
    (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
    s
a : E
ha :
  Membership.mem (γ := Multiset E)
    (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))) a
has : (spectralMulAlgNorm K E : (a : E) → ℝ) a = s
rw : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = s
⊢ r = s
have rw₁ : Eq (α := ℝ) ((spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) : ℝ)
  ((spectralMulAlgNorm K E : (a : E) → ℝ) a : ℝ)
Tactic: rw [← hr, ← has, spectralMulAlgNorm_eq_of_mem_roots K L x ha]
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
r : ℝ
hr : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
s : ℝ
hs :
  Membership.mem (γ := Multiset ℝ)
    (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
    s
a : E
ha :
  Membership.mem (γ := Multiset E)
    (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))) a
has : (spectralMulAlgNorm K E : (a : E) → ℝ) a = s
rw : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = s
rw₁ :
  Eq (α := ℝ) ((spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) : ℝ)
    ((spectralMulAlgNorm K E : (a : E) → ℝ) a : ℝ)
⊢ r = s
have rw₂ : Eq (α := ℝ) ((spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) : ℝ)
  ((spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) : ℝ)
Tactic: rw [← hr, ← has, spectralMulAlgNorm_eq_of_mem_roots K L x ha]
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
r : ℝ
hr : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
⊢ natDegree (minpoly K x) =
    Multiset.count r
      (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
        (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
have h : ∀ (s : ℝ),
  Membership.mem (γ := Multiset ℝ)
      (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
        (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
      s →
    r = s
Tactic: have h : ∀ s ∈ Multiset.map (spectralMulAlgNorm K E) ((mapAlg K E) (minpoly K x)).roots,
        r = s := by
      intro s hs
      obtain ⟨a, ha, has⟩ := Multiset.mem_map.mp hs
      rw [← hr, ← has, spectralMulAlgNorm_eq_of_mem_roots K L x ha]
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
r : ℝ
hr : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
h :
  ∀ (s : ℝ),
    Membership.mem (γ := Multiset ℝ)
        (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
          (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
        s →
      r = s
⊢ natDegree (minpoly K x) =
    Multiset.count r
      (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
        (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
have pos : natDegree (minpoly K x) =
  Multiset.card (α := ℝ)
    (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
Tactic: rwa [Multiset.count_eq_card.mpr h, Multiset.card_map]
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
r : ℝ
hr : ¬(spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
⊢ 0 =
    Multiset.count r
      (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
        (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
have neg : r ∉
  Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
    (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
Tactic: rw [Multiset.count_eq_zero_of_notMem]
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
r : ℝ
hr : ¬(spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
hr_mem :
  Membership.mem (γ := Multiset ℝ)
    (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
    r
⊢ False
have neg : ∀ (e : E)
  (he :
    Membership.mem (γ := Multiset E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))) e)
  (her : (spectralMulAlgNorm K E : (a : E) → ℝ) e = r), False
Tactic: obtain ⟨e, he, her⟩ := Multiset.mem_map.mp hr_mem
-- 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
hu : IsUltrametricDist K
inst_3 : CompleteSpace K
x : L
E : Type u_2
inst_4 : Field E
inst_5 : Algebra K E
inst_6 : Algebra L E
inst_7 : IsScalarTower K L E
inst_8 : IsSplittingField L E (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
inst_9 : Algebra.IsAlgebraic K E
h_deg :
  natDegree (minpoly K x) =
    Multiset.card.{u_2} (α := E)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x)))
r : ℝ
hr : ¬(spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
hr_mem :
  Membership.mem (γ := Multiset ℝ)
    (Multiset.map (α := E) (⇑(spectralMulAlgNorm K E) : (a : E) → ℝ)
      (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))))
    r
e : E
he :
  Membership.mem (γ := Multiset E)
    (roots (((mapAlg K E : AlgHom.{u, u, u_2} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))) e
her : (spectralMulAlgNorm K E : (a : E) → ℝ) e = r
⊢ False
have her₁ : (spectralMulAlgNorm K E : (a : E) → ℝ) ((algebraMap L E : (a : L) → E) x : E) = r
Tactic: rw [spectralMulAlgNorm_eq_of_mem_roots K L x he] at her
Cleared hypotheses: her
-- 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 : L
E : Type v := SplittingField (K := L) (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
⊢ spectralNorm K L x = ‖coeff (minpoly K x) 0‖ ^ HDiv.hDiv (α := ℝ) 1 (↑(natDegree (minpoly K x)) : ℝ)
have hspl : Splits.{v} (R := E) (((mapAlg K E : AlgHom.{u, u, v} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
Tactic: have hspl : Splits (mapAlg K E (minpoly K x)) :=
    IsSplittingField.IsScalarTower.splits (K := L) E (minpoly K 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 : L
E : Type v := SplittingField (K := L) (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
hspl : Splits.{v} (R := E) (((mapAlg K E : AlgHom.{u, u, v} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
⊢ spectralNorm K L x = ‖coeff (minpoly K x) 0‖ ^ HDiv.hDiv (α := ℝ) 1 (↑(natDegree (minpoly K x)) : ℝ)
have this : Algebra.IsAlgebraic L E
Tactic: have : Algebra.IsAlgebraic L E :=
    IsSplittingField.IsScalarTower.isAlgebraic E (mapAlg K L (minpoly K 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 : L
E : Type v := SplittingField (K := L) (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
hspl : Splits.{v} (R := E) (((mapAlg K E : AlgHom.{u, u, v} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
this : Algebra.IsAlgebraic L E
⊢ spectralNorm K L x = ‖coeff (minpoly K x) 0‖ ^ HDiv.hDiv (α := ℝ) 1 (↑(natDegree (minpoly K x)) : ℝ)
have this₁ : Algebra.IsAlgebraic K E
Tactic: have : Algebra.IsAlgebraic K E := Algebra.IsAlgebraic.trans K L E
-- 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 : L
E : Type v := SplittingField (K := L) (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
hspl : Splits.{v} (R := E) (((mapAlg K E : AlgHom.{u, u, v} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
this_1 : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
⊢ spectralNorm K L x = ‖coeff (minpoly K x) 0‖ ^ HDiv.hDiv (α := ℝ) 1 (↑(natDegree (minpoly K x)) : ℝ)
have rw : Monic.{v} (R := E) (((mapAlg K E : AlgHom.{u, u, v} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
Tactic: rw [one_div, Real.eq_rpow_inv (spectralNorm_nonneg x) (norm_nonneg ((minpoly K x).coeff 0)),
    Real.rpow_natCast, @spectralNorm.eq_of_tower K _ E,
    ← @spectralNorm_extends K _ L _ _ ((minpoly K x).coeff 0),
    @spectralNorm.eq_of_tower K _ E _ _ L, ← spectralMulAlgNorm_def,
    ← spectralMulAlgNorm_def, Polynomial.coeff_zero_of_isScalarTower,
    hspl.coeff_zero_eq_prod_roots_of_monic _, map_mul, map_pow,
    map_neg_eq_map, map_one, one_pow, one_mul, spectralNorm_pow_natDegree_eq_prod_roots _ _ x]
-- 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 : L
E : Type v := SplittingField (K := L) (((mapAlg K L : AlgHom.{u, u, v} K K[X] L[X]) : (a : K[X]) → L[X]) (minpoly K x))
hspl : Splits.{v} (R := E) (((mapAlg K E : AlgHom.{u, u, v} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
this_1 : Algebra.IsAlgebraic L E
this : Algebra.IsAlgebraic K E
rw : Monic.{v} (R := E) (((mapAlg K E : AlgHom.{u, u, v} K K[X] E[X]) : (a : K[X]) → E[X]) (minpoly K x))
⊢ spectralNorm K L x = ‖coeff (minpoly K x) 0‖ ^ HDiv.hDiv (α := ℝ) 1 (↑(natDegree (minpoly K x)) : ℝ)
have rw₁ : Ne (α := ℝ) (↑(natDegree (minpoly K x)) : ℝ) 0
Tactic: rw [one_div, Real.eq_rpow_inv (spectralNorm_nonneg x) (norm_nonneg ((minpoly K x).coeff 0)),
    Real.rpow_natCast, @spectralNorm.eq_of_tower K _ E,
    ← @spectralNorm_extends K _ L _ _ ((minpoly K x).coeff 0),
    @spectralNorm.eq_of_tower K _ E _ _ L, ← spectralMulAlgNorm_def,
    ← spectralMulAlgNorm_def, Polynomial.coeff_zero_of_isScalarTower,
    hspl.coeff_zero_eq_prod_roots_of_monic _, map_mul, map_pow,
    map_neg_eq_map, map_one, one_pow, one_mul, spectralNorm_pow_natDegree_eq_prod_roots _ _ x]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
⊢ IsIntegralCurveAt γ v t₀ ↔ ∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s
have rw : (∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y) ↔ ∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s
Tactic: rw [IsIntegralCurveAt, Filter.eventually_iff_exists_mem]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
⊢ (∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y) ↔ ∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s
have refine : (∃ s ∈ 𝓝 t₀, IsIntegralCurveOn γ v s) → ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y
Tactic: refine ⟨fun ⟨s, hs, h⟩ ↦ ⟨s, hs, fun t ht ↦ (h t ht).hasDerivWithinAt⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.Basic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsIntegralCurveOn γ v s
⊢ ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y
have hs₁ : ∃ t ⊆ s, IsOpen t ∧ t₀ ∈ t
Tactic: rw [mem_nhds_iff] at hs
Cleared hypotheses: hs, h
-- Lean 4 proof step from Mathlib.Analysis.ODE.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
hs : ∃ t ⊆ s, IsOpen t ∧ t₀ ∈ t
h : IsIntegralCurveOn γ v s
⊢ ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y
have obtain : ∀ (s' : Set ℝ) (h₁ : s' ⊆ s) (h₂ : IsOpen s') (h₃ : t₀ ∈ s'), ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y
Tactic: obtain ⟨s', h₁, h₂, h₃⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.ODE.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
h : IsIntegralCurveOn γ v s
s' : Set ℝ
h₁ : s' ⊆ s
h₂ : IsOpen s'
h₃ : t₀ ∈ s'
⊢ ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasDerivAt γ (v y (γ y)) y
have refine : ∀ y ∈ s', HasDerivAt γ (v y (γ y)) y
Tactic: refine ⟨s', h₂.mem_nhds h₃, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
h : IsIntegralCurveOn γ v s
s' : Set ℝ
h₁ : s' ⊆ s
h₂ : IsOpen s'
h₃ : t₀ ∈ s'
t : ℝ
ht : t ∈ s'
⊢ HasDerivAt γ (v t (γ t)) t
have apply : s ∈ 𝓝 t
Tactic: apply (h t (h₁ ht)).hasDerivAt
-- Lean 4 proof step from Mathlib.Analysis.ODE.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
s : Set ℝ
h : IsIntegralCurveOn γ v s
s' : Set ℝ
h₁ : s' ⊆ s
h₂ : IsOpen s'
h₃ : t₀ ∈ s'
t : ℝ
ht : t ∈ s'
⊢ s ∈ 𝓝 t
have rw : ∃ t_1 ⊆ s, IsOpen t_1 ∧ t ∈ t_1
Tactic: rw [mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
⊢ IsIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)
have rw : (∃ ε > 0, ∀ y ∈ Metric.ball t₀ ε, HasDerivAt γ (v y (γ y)) y) ↔ ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)
Tactic: rw [IsIntegralCurveAt, Metric.eventually_nhds_iff_ball]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ : ℝ
⊢ (∃ ε > 0, ∀ y ∈ Metric.ball t₀ ε, HasDerivAt γ (v y (γ y)) y) ↔ ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)
have a : ∀ (ε y : ℝ) (hy : y ∈ Metric.ball t₀ ε),
  HasDerivAt γ (v y (γ y)) y ↔ HasDerivWithinAt γ (v y (γ y)) (Metric.ball t₀ ε) y
Tactic: congrm ∃ ε > 0, ∀ (y : ℝ) (hy : y ∈ Metric.ball t₀ ε), ?_
-- Lean 4 proof step from Mathlib.Analysis.ODE.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
h : ∀ (t : ℝ), IsIntegralCurveAt γ v t
t : ℝ
⊢ HasDerivAt γ (v t (γ t)) t
have obtain : ∀ (s : Set ℝ) (hs : s ∈ 𝓝 t) (h : IsIntegralCurveOn γ v s), HasDerivAt γ (v t (γ t)) t
Tactic: obtain ⟨s, hs, h⟩ := isIntegralCurveAt_iff_exists_mem_nhds.mp (h t)