awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : S.Nonempty
⊢ Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ ≤ ‖a - a'‖
have pos : Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ‖a - a'‖
Tactic: apply Finset.min'_le (S.image fun x => ‖a - x‖) (‖a - a'‖)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : S.Nonempty
⊢ Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ‖a - a'‖
have pos : a' ∈ S
Tactic: apply Finset.mem_image_of_mem
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : S.Nonempty
⊢ a' ∈ S
have pos : a' ∈ rootSet (minpoly L a) F ∧ a' ≠ a
Tactic: simp only [minpoly.eq_of_irreducible_of_monic firr fa0 fmon, Finset.mem_filter,
        Set.mem_toFinset, S]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : S.Nonempty
⊢ a' ∈ rootSet (minpoly L a) F ∧ a' ≠ a
have pos : IsConjRoot L a a' ∧ a' ≠ a
Tactic: rw [← (isConjRoot_iff_mem_minpoly_rootSet ⟨f, fmon, fa0⟩)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : ¬S.Nonempty
⊢ 1 ≤ ‖a - a'‖
have hS₁ : ∀ ⦃x : F⦄, x ∈ f.rootSet F → x = a
Tactic: simp only [ne_eq, Finset.not_nonempty_iff_eq_empty, Finset.filter_eq_empty_iff,
      Set.mem_toFinset, not_not, S] at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
a' : F
conj : IsConjRoot L a a'
ne : a ≠ a'
hS : ∀ ⦃x : F⦄, x ∈ f.rootSet F → x = a
⊢ 1 ≤ ‖a - a'‖
have conj₁ : Membership.mem (γ := Set f.SplittingField) (f.rootSet f.SplittingField) a'
Tactic: rw [isConjRoot_iff_mem_minpoly_rootSet ⟨f, fmon, fa0⟩,
          ← minpoly.eq_of_irreducible_of_monic firr fa0 fmon] at conj
Cleared hypotheses: conj, ne, hS
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
⊢ ∃ (x : L), eval x f = 0
have norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
Tactic: have norm_sub_le : ∀ a' : F, IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖ := by
    intro a' conj ne
    by_cases hS : S.Nonempty <;> simp only [hS, ↓reduceDIte, δ]
    · apply Finset.min'_le (S.image fun x => ‖a - x‖) (‖a - a'‖)
      apply Finset.mem_image_of_mem
      simp only [minpoly.eq_of_irreducible_of_monic firr fa0 fmon, Finset.mem_filter,
        Set.mem_toFinset, S]
      rw [← (isConjRoot_iff_mem_minpoly_rootSet ⟨f, fmon, fa0⟩)]
      exact ⟨conj, ne.symm⟩
    · simp only [ne_eq, Finset.not_nonempty_iff_eq_empty, Finset.filter_eq_empty_iff,
      Set.mem_toFinset, not_not, S] at hS
      rw [isConjRoot_iff_mem_minpoly_rootSet ⟨f, fmon, fa0⟩,
          ← minpoly.eq_of_irreducible_of_monic firr fa0 fmon] at conj
      exact (ne (hS conj).symm).elim
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
⊢ δ > 0
have pos : ∀ (hS : S.Nonempty), δ > 0
Tactic: by_cases hS : S.Nonempty
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
pos : ∀ (hS : S.Nonempty), δ > 0
⊢ δ > 0
have neg : ∀ (hS : ¬S.Nonempty), δ > 0
Tactic: by_cases hS : S.Nonempty
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : S.Nonempty
⊢ δ > 0
have pos : GT.gt (α := ℝ) (Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) sorry) 0
Tactic: simp only [hS, ↓reduceDIte, δ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : ¬S.Nonempty
⊢ δ > 0
have neg : GT.gt (α := ℝ) 1 0
Tactic: simp only [hS, ↓reduceDIte, δ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : S.Nonempty
⊢ GT.gt (α := ℝ) (Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯) 0
have pos : ∀ a_1 ∈ S, 0 < ‖a - a_1‖
Tactic: simp only [gt_iff_lt, Finset.lt_min'_iff, Finset.mem_image, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : S.Nonempty
a' : f.SplittingField
ha' : a' ∈ S
⊢ 0 < ‖a - a'‖
have ha'₁ : a' ∈ f.rootSet F ∧ a' ≠ a
Tactic: simp only [Finset.mem_filter, Set.mem_toFinset, S] at ha'
Cleared hypotheses: ha'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : S.Nonempty
a' : f.SplittingField
ha' : a' ∈ f.rootSet F ∧ a' ≠ a
⊢ 0 < ‖a - a'‖
have pos : a ≠ a'
Tactic: rw [norm_pos_iff, sub_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : ¬S.Nonempty
⊢ GT.gt (α := ℝ) 1 0
have linarith : LE.le (α := ℝ) 1 0 → -1 + HSub.hSub (α := ℝ) 1 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
⊢ ∃ (x : L), eval x f = 0
have δpos : δ > 0
Tactic: have δpos : δ > 0 := by
    by_cases hS : S.Nonempty <;> simp only [hS, ↓reduceDIte, δ]
    · simp only [gt_iff_lt, Finset.lt_min'_iff, Finset.mem_image, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      rintro a' ha'
      simp only [Finset.mem_filter, Set.mem_toFinset, S] at ha'
      rw [norm_pos_iff, sub_ne_zero]
      exact ha'.2.symm
    · linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
δpos : δ > 0
⊢ ∃ (x : L), eval x f = 0
have hε : (δ / max ‖a‖ 1) ^ f.natDegree / HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 > 0
Tactic: have hε : (δ / (max ‖a‖ 1)) ^ f.natDegree / (f.natDegree + 1) > 0 := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
δpos : δ > 0
hε : (δ / max ‖a‖ 1) ^ f.natDegree / HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 > 0
⊢ ∃ (x : L), eval x f = 0
have H : ∀ (g : K[X]) (gmon : g.Monic) (gdeg : f.natDegree = g.natDegree)
  (gcoeff :
    ∀ (n : ℕ),
      ‖coeff (map (algebraMap K L) g) n - f.coeff n‖ <
        (δ / max ‖a‖ 1) ^ f.natDegree / HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1),
  ∃ (x : L), eval x f = 0
Tactic: obtain ⟨g, gmon, gdeg, gcoeff⟩ :=
    exists_monic_and_natDegree_eq_and_norm_map_algebraMap_coeff_sub_lt hi fmon hε
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
δpos : δ > 0
hε : (δ / max ‖a‖ 1) ^ f.natDegree / HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 > 0
g : K[X]
gmon : g.Monic
gdeg : f.natDegree = g.natDegree
gcoeff :
  ∀ (n : ℕ),
    ‖coeff (map (algebraMap K L) g) n - f.coeff n‖ <
      (δ / max ‖a‖ 1) ^ f.natDegree / HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1
⊢ ∃ (x : L), eval x f = 0
have H : ∀ (b : f.SplittingField)
  (hb : Membership.mem (γ := Multiset f.SplittingField) (aroots (map (algebraMap K L) g) f.SplittingField) b)
  (hab :
    ‖a - b‖ <
      HPow.hPow (β := ℝ)
          (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 *
            ((δ / max ‖a‖ 1) ^ f.natDegree / HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1))
          (↑f.natDegree : ℝ)⁻¹ *
        max ‖a‖ 1),
  ∃ (x : L), eval x f = 0
Tactic: let ⟨b, hb, hab⟩ := exists_aroots_norm_sub_lt_of_norm_coeff_sub_lt
      hε fa0 fmon (gmon.map _) (gdeg ▸ (g.natDegree_map _)) gcoeff
      (by simpa [Polynomial.map_map] using (IsAlgClosed.splits g).map ((algebraMap L F).comp _))