awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
this_2 : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : Membership.mem (γ := IntermediateField K L) K⟮y⟯ z ↔ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : z' = (σ.symm : (a : L) → L) z
⊢ max ‖z‖ ‖z'‖ ≤ ‖x - y‖
have simp : spectralNorm K L z ≤ spectralNorm K L (x - y) ∧
  spectralNorm K L ((σ.symm : (a : L) → L) z : L) ≤ spectralNorm K L (x - y)
Tactic: simp only [NormedAlgebra.norm_eq_spectralNorm K, hσ, sup_le_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
this_2 : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : Membership.mem (γ := IntermediateField K L) K⟮y⟯ z ↔ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : z' = (σ.symm : (a : L) → L) z
⊢ spectralNorm K L z ≤ spectralNorm K L (x - y) ∧
    spectralNorm K L ((σ.symm : (a : L) → L) z : L) ≤ spectralNorm K L (x - y)
have rw : spectralNorm K L z ≤ spectralNorm K L (x - y) ∧ spectralNorm K L z ≤ spectralNorm K L (x - y)
Tactic: rw [← AlgEquiv.restrictScalars_apply K,
              ← spectralNorm_eq_of_equiv (σ.symm.restrictScalars K)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
this_2 : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : Membership.mem (γ := IntermediateField K L) K⟮y⟯ z ↔ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : z' = (σ.symm : (a : L) → L) z
⊢ ‖x - y‖ < ‖x - (z' + y)‖
have a : IsConjRoot K x (z' + y)
Tactic: apply kr (z' + y)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
this_2 : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : Membership.mem (γ := IntermediateField K L) K⟮y⟯ z ↔ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : z' = (σ.symm : (a : L) → L) z
a : IsConjRoot K x (z' + y)
⊢ ‖x - y‖ < ‖x - (z' + y)‖
have a₁ : x ≠ z' + y
Tactic: apply kr (z' + y)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
this_2 : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : Membership.mem (γ := IntermediateField K L) K⟮y⟯ z ↔ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : z' = (σ.symm : (a : L) → L) z
⊢ IsConjRoot K x (z' + y)
have a : IsConjRoot (↥K⟮y⟯) x (z' + y)
Tactic: apply IsConjRoot.of_isScalarTower (L := K⟮y⟯) xsep.isIntegral
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
this_2 : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : Membership.mem (γ := IntermediateField K L) K⟮y⟯ z ↔ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : z' = (σ.symm : (a : L) → L) z
⊢ ‖x - (z' + y)‖ = ‖z - z'‖
have e_a : x - (z' + y) = z - z'
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
this_2 : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : Membership.mem (γ := IntermediateField K L) K⟮y⟯ z ↔ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : z' = (σ.symm : (a : L) → L) z
⊢ False
have this₁ : ‖z - z'‖ < ‖z - z'‖
Tactic: have : ‖z - z'‖ < ‖z - z'‖ :=
      calc
        _ ≤ max ‖z‖ ‖z'‖ := by
          simpa [norm_neg, sub_eq_add_neg] using (IsUltrametricDist.norm_add_le_max z (- z'))
        _ ≤ ‖x - y‖ := by
          simp only [NormedAlgebra.norm_eq_spectralNorm K, hσ, sup_le_iff]
          rw [← AlgEquiv.restrictScalars_apply K,
              ← spectralNorm_eq_of_equiv (σ.symm.restrictScalars K)]
          simp [z]
        _ < ‖x - (z' + y)‖ := by
          apply kr (z' + y)
          · apply IsConjRoot.of_isScalarTower (L := K⟮y⟯) xsep.isIntegral
            simpa [z, y'] using IsConjRoot.add_algebraMap y' h1
          · simpa [z, sub_eq_iff_eq_add] using hne
        _ = ‖z - z'‖ := by congr 1; ring
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
⊢ Membership.mem (γ := IntermediateField K L) K⟮y⟯ x
have norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
Tactic: have norm_iL (x : L) : ‖iL x‖ = ‖x‖ := norm_algebraMap' _ _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
⊢ Membership.mem (γ := IntermediateField K L) K⟮y⟯ x
have suffices : Membership.mem (α := C) (γ := IntermediateField K C) K⟮((iL : (a : L) → C) y : C)⟯ ((iL : (a : L) → C) x : C)
Tactic: suffices this : iL x ∈ K⟮iL y⟯ by
      simpa [← Set.image_singleton, ← IntermediateField.adjoin_map] using this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
⊢ Membership.mem (α := C) (γ := IntermediateField K C) K⟮((iL : (a : L) → C) y : C)⟯ ((iL : (a : L) → C) x : C)
have refine_1 : (Polynomial.map (algebraMap K C) (minpoly K (B := C) ((iL : (a : L) → C) x : C))).Splits
Tactic: refine IsKrasner.krasner ((xsep.map _ iL.injective).of_dvd dvd_rfl) ?_ (yint.map iL) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
refine_1 : (Polynomial.map (algebraMap K C) (minpoly K (B := C) ((iL : (a : L) → C) x : C))).Splits
⊢ Membership.mem (α := C) (γ := IntermediateField K C) K⟮((iL : (a : L) → C) y : C)⟯ ((iL : (a : L) → C) x : C)
have refine_2 : ∀ (x' : C),
  IsConjRoot K ((iL : (a : L) → C) x) x' →
    (iL : (a : L) → C) x ≠ x' →
      ‖HSub.hSub (α := C) (β := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) y : C)‖ <
        ‖HSub.hSub (α := C) ((iL : (a : L) → C) x : C) x'‖
Tactic: refine IsKrasner.krasner ((xsep.map _ iL.injective).of_dvd dvd_rfl) ?_ (yint.map iL) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
xC' : C
hx' : IsConjRoot K ((iL : (a : L) → C) x) xC'
hne : (iL : (a : L) → C) x ≠ xC'
⊢ xC' ∈ Polynomial.rootSet (minpoly K x) C
have rwa : ∀ (hx' : xC' ∈ Polynomial.rootSet (minpoly K (B := C) ((iL : (a : L) → C) x : C)) C) (hne : (iL : (a : L) → C) x ≠ xC'),
  xC' ∈ Polynomial.rootSet (minpoly K x) C
Tactic: rwa [isConjRoot_iff_mem_minpoly_rootSet (xsep.isIntegral.map _),
          minpoly.algHom_eq iL iL.injective x] at hx'
Cleared hypotheses: hx', hne
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
xC' : C
hx' : IsConjRoot K ((iL : (a : L) → C) x) xC'
hne : (iL : (a : L) → C) x ≠ xC'
rwa :
  ∀ (hx' : xC' ∈ Polynomial.rootSet (minpoly K (B := C) ((iL : (a : L) → C) x : C)) C)
    (hne : (iL : (a : L) → C) x ≠ xC'), xC' ∈ Polynomial.rootSet (minpoly K x) C
⊢ xC' ∈ Polynomial.rootSet (minpoly K x) C
have rwa₁ : ∀ (hx' : xC' ∈ Polynomial.rootSet (minpoly K x) C) (hne : (iL : (a : L) → C) x ≠ xC'),
  xC' ∈ Polynomial.rootSet (minpoly K x) C
Tactic: rwa [isConjRoot_iff_mem_minpoly_rootSet (xsep.isIntegral.map _),
          minpoly.algHom_eq iL iL.injective x] at hx'
Cleared hypotheses: hx', hne
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
xC' : C
hx' : IsConjRoot K ((iL : (a : L) → C) x) xC'
hne : (iL : (a : L) → C) x ≠ xC'
⊢ ‖HSub.hSub (α := C) (β := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) y : C)‖ <
    ‖HSub.hSub (α := C) ((iL : (a : L) → C) x : C) xC'‖
have this₁ : xC' ∈ Polynomial.rootSet (minpoly K x) C
Tactic: have : xC' ∈ (minpoly K x).rootSet C := by
        rwa [isConjRoot_iff_mem_minpoly_rootSet (xsep.isIntegral.map _),
          minpoly.algHom_eq iL iL.injective x] at hx'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this_4 : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
xC' : C
hx' : IsConjRoot K ((iL : (a : L) → C) x) xC'
hne : (iL : (a : L) → C) x ≠ xC'
this : xC' ∈ Polynomial.rootSet (minpoly K x) C
⊢ ‖HSub.hSub (α := C) (β := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) y : C)‖ <
    ‖HSub.hSub (α := C) ((iL : (a : L) → C) x : C) xC'‖
have this₁ : ∃ x_1 ∈ Polynomial.rootSet (minpoly K x) L, (iL : (a : L) → C) x_1 = xC'
Tactic: simp only [← sp.image_rootSet iL, Set.mem_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this_4 : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
xC' : C
hx' : IsConjRoot K ((iL : (a : L) → C) x) xC'
hne : (iL : (a : L) → C) x ≠ xC'
this : ∃ x_1 ∈ Polynomial.rootSet (minpoly K x) L, (iL : (a : L) → C) x_1 = xC'
⊢ ‖HSub.hSub (α := C) (β := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) y : C)‖ <
    ‖HSub.hSub (α := C) ((iL : (a : L) → C) x : C) xC'‖
have refine_2 : ∀ (c : L) (hc : c ∈ Polynomial.rootSet (minpoly K x) L)
  (hx' : IsConjRoot K (A := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C))
  (hne : Ne.{u_1 + 1} (α := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)),
  ‖HSub.hSub (α := C) (β := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) y : C)‖ <
    ‖HSub.hSub (α := C) (β := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)‖
Tactic: obtain ⟨c, hc, rfl⟩ := this
Cleared hypotheses: xC', hx', hne, this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
c : L
hc : c ∈ Polynomial.rootSet (minpoly K x) L
hx' : IsConjRoot K (A := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)
hne : Ne.{u_1 + 1} (α := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)
⊢ ‖HSub.hSub (α := C) (β := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) y : C)‖ <
    ‖HSub.hSub (α := C) (β := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)‖
have hc₁ : IsConjRoot K x c
Tactic: rw [← isConjRoot_iff_mem_minpoly_rootSet xsep.isIntegral] at hc
Cleared hypotheses: hc, hx', hne
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
⊢ (cobounded α)⁻¹ = 𝓝[≠] 0
have rw : Eq.{u_1 + 1} (α := Filter α) (comap Inv.inv (comap norm atTop)) (comap norm (comap Inv.inv atTop))
Tactic: rw [← comap_norm_atTop, ← Filter.comap_inv, ← comap_norm_nhdsGT_zero, ← inv_atTop₀,
    ← Filter.comap_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
⊢ (𝓝[≠] 0)⁻¹ = cobounded α
have rw : (cobounded α)⁻¹⁻¹ = cobounded α
Tactic: rw [← inv_cobounded₀, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
rw : (cobounded α)⁻¹⁻¹ = cobounded α
⊢ (𝓝[≠] 0)⁻¹ = cobounded α
have rw₁ : cobounded α = cobounded α
Tactic: rw [← inv_cobounded₀, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
⊢ UniformContinuousOn Inv.inv s
have rw : ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε
Tactic: rw [Metric.uniformContinuousOn_iff_le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε
have rcases : ∀ (r : ℝ) (hr₀ : 0 < r) (hr : {y : α | ‖y‖ < r} ⊆ sᶜ), ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε
Tactic: rcases NormedAddGroup.nhds_zero_basis_norm_lt.mem_iff.mp hs with ⟨r, hr₀, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (hypothesis)
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : {y : α | ‖y‖ < r} ⊆ sᶜ
⊢ ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε
have hr₁ : s ⊆ {a : α | r ≤ ‖a‖}
Tactic: simp only [Set.subset_compl_comm (t := s), Set.compl_setOf, not_lt] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (hypothesis)
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a : α | r ≤ ‖a‖}
⊢ ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε
have hs₀ : ∀ x ∈ s, x ≠ 0
Tactic: have hs₀ : ∀ x ∈ s, x ≠ 0 := fun x hx ↦ norm_pos_iff.mp <| hr₀.trans_le (hr hx)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Lemmas (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
s : Set α
hs : Membership.mem (γ := Filter α) (𝓝 0) sᶜ
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a : α | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
⊢ ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε
have refine : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s) (hxy : dist x y ≤ ε * HPow.hPow (β := ℕ) r 2), dist x⁻¹ y⁻¹ ≤ ε
Tactic: refine ⟨ε * r ^ 2, by positivity, fun x hx y hy hxy ↦ ?_⟩