awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst : DenselyNormedField α
x y : α
hxy :
  LT.lt (α := (↑(Set.range.{0, u_2 + 1} (ι := α) nnnorm) : Type))
    (Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖x‖₊ ⋯)
    (Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖y‖₊ ⋯)
z : α
h :
  (↑(Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖x‖₊ ⋯) : ℝ≥0) < ‖z‖₊ ∧
    ‖z‖₊ < (↑(Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖y‖₊ ⋯) : ℝ≥0)
⊢ ∃ (a : (↑(Set.range.{0, u_2 + 1} (ι := α) nnnorm) : Type)),
    Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖x‖₊ ⋯ < a ∧
      a < Subtype.mk (p := fun (x : ℝ≥0) ↦ x ∈ Set.range.{0, u_2 + 1} (ι := α) nnnorm) ‖y‖₊ ⋯

Tactic:
exact ⟨⟨‖z‖₊, z, rfl⟩, h⟩
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
h : ∃ (x : 𝕜), x ≠ 0 ∧ ‖x‖ ≠ 1
rcases : ∀ (x : 𝕜) (hx : x ≠ 0) (hx1 : ‖x‖ ≠ 1), ∃ (x : 𝕜), 1 < ‖x‖
⊢ ∃ (x : 𝕜), 1 < ‖x‖

Tactic:
rcases h with ⟨x, hx, hx1⟩
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
x : 𝕜
hx : x ≠ 0
hx1 : ‖x‖ ≠ 1
inl : ∀ (hlt : ‖x‖ < 1), ∃ (x : 𝕜), 1 < ‖x‖
inr : ∀ (hlt : 1 < ‖x‖), ∃ (x : 𝕜), 1 < ‖x‖
⊢ ∃ (x : 𝕜), 1 < ‖x‖

Tactic:
rcases hx1.lt_or_gt with hlt | hlt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
x : 𝕜
hx : x ≠ 0
hx1 : ‖x‖ ≠ 1
hlt : ‖x‖ < 1
h : 1 < ‖x⁻¹‖
⊢ ∃ (x : 𝕜), 1 < ‖x‖

Tactic:
use x⁻¹
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
x : 𝕜
hx : x ≠ 0
hx1 : ‖x‖ ≠ 1
hlt : ‖x‖ < 1
h : 1 < ‖x‖⁻¹
⊢ 1 < ‖x⁻¹‖

Tactic:
rw [norm_inv]

Premises used: norm_inv
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
x : 𝕜
hx : x ≠ 0
hx1 : ‖x‖ ≠ 1
hlt : ‖x‖ < 1
⊢ 1 < ‖x‖⁻¹

Tactic:
(one_lt_inv₀ (norm_pos_iff.2 hx)).2 hlt

Premises used: Iff.mpr, norm_pos_iff, one_lt_inv₀
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
x : 𝕜
hx : x ≠ 0
hx1 : ‖x‖ ≠ 1
hlt : ‖x‖ < 1
⊢ 1 < ‖x‖⁻¹

Tactic:
exact (one_lt_inv₀ (norm_pos_iff.2 hx)).2 hlt

Premises used: Iff.mpr, norm_pos_iff, one_lt_inv₀
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
x : 𝕜
hx : x ≠ 0
hx1 : ‖x‖ ≠ 1
hlt : 1 < ‖x‖
⊢ ∃ (x : 𝕜), 1 < ‖x‖

Tactic:
⟨x, hlt⟩

Premises used: Exists.intro
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
x : 𝕜
hx : x ≠ 0
hx1 : ‖x‖ ≠ 1
hlt : 1 < ‖x‖
⊢ ∃ (x : 𝕜), 1 < ‖x‖

Tactic:
exact ⟨x, hlt⟩
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
x_1 x_2 : ℝ
h₀ : 0 ≤ x_1
hr : x_1 < x_2
x : ℝ
h : x_1 < x ∧ x < x_2
rwa : x_1 < |x| ∧ |x| < x_2
rwa₁ rwa₂ rwa₃ rwa₄ : x_1 < x ∧ x < x_2
⊢ x_1 < ‖x‖ ∧ ‖x‖ < x_2

Tactic:
rwa [Real.norm_eq_abs, abs_of_nonneg (h₀.trans h.1.le)]

Premises used: LT.lt.le, And.left, abs_of_nonneg, LE.le.trans, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
x y : ℝ
hx : 0 ≤ x
a : (↑(x.toNNReal * ‖y‖₊) : ℝ) = (↑‖x * y‖₊ : ℝ)
⊢ x.toNNReal * ‖y‖₊ = ‖x * y‖₊

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
x y : ℝ
hx : 0 ≤ x
⊢ (↑(x.toNNReal * ‖y‖₊) : ℝ) = (↑‖x * y‖₊ : ℝ)

Tactic:
simp only [NNReal.coe_mul, nnnorm_mul, coe_nnnorm, Real.toNNReal_of_nonneg, norm_of_nonneg, hx,
    NNReal.coe_mk]

Premises used: NNReal.coe_mk, coe_nnnorm, Real.toNNReal_of_nonneg, NNReal.coe_mul, nnnorm_mul, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Normed.Field.Basic
Goal:
x y : ℝ
hy : 0 ≤ y
rw : y.toNNReal * ‖x‖₊ = ‖x * y‖₊
rw₁ : y.toNNReal * ‖x‖₊ = ‖y * x‖₊
rw₂ rw₃ : ‖y * x‖₊ = ‖y * x‖₊
⊢ ‖x‖₊ * y.toNNReal = ‖x * y‖₊

Tactic:
rw [mul_comm, mul_comm x, toNNReal_mul_nnnorm x hy]

Premises used: Real.toNNReal_mul_nnnorm, mul_comm
-- Module: Mathlib.Analysis.Normed.Field.Dense
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
H : ∀ (p : L[X]), p.Monic → Irreducible p → ∃ (x : L), eval x p = 0
⊢ IsAlgClosed L

Tactic:
apply IsAlgClosed.of_exists_root

Premises used: IsAlgClosed.of_exists_root
-- Module: Mathlib.Analysis.Normed.Field.Dense
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
⊢ f.natDegree ≠ 0

Tactic:
have fnatdeg0 : f.natDegree ≠ 0 := (Irreducible.natDegree_pos firr).ne'
-- Module: Mathlib.Analysis.Normed.Field.Dense
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
⊢ degree (R := f.SplittingField) (map (algebraMap L f.SplittingField) f) ≠ 0

Tactic:
simpa using degree_ne_of_natDegree_ne fnatdeg0

Premises used: Polynomial.degree_ne_of_natDegree_ne
-- Module: Mathlib.Analysis.Normed.Field.Dense
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 ⋯ ⋯
rw : eval a (map (algebraMap L f.SplittingField) f) = 0
⊢ Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0

Tactic:
rw [← eval_map_algebraMap]

Premises used: Polynomial.eval_map_algebraMap
-- Module: Mathlib.Analysis.Normed.Field.Dense
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 ⋯ ⋯
⊢ degree (R := f.SplittingField) (map (algebraMap L f.SplittingField) f) ≠ 0

Tactic:
simpa using degree_ne_of_natDegree_ne fnatdeg0

Premises used: Polynomial.degree_ne_of_natDegree_ne
-- Module: Mathlib.Analysis.Normed.Field.Dense
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 ⋯ ⋯
⊢ eval a (map (algebraMap L f.SplittingField) f) = 0

Tactic:
exact eval_rootOfSplits (Polynomial.SplittingField.splits f)
      (by simpa using degree_ne_of_natDegree_ne fnatdeg0)

Premises used: Polynomial.SplittingField.splits, Polynomial.eval_rootOfSplits
-- Module: Mathlib.Analysis.Normed.Field.Dense
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 ⋯ ⋯
⊢ Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0

Tactic:
have fa0 : f.aeval a = 0 := by
    rw [← eval_map_algebraMap]
    exact eval_rootOfSplits (Polynomial.SplittingField.splits f)
      (by simpa using degree_ne_of_natDegree_ne fnatdeg0)
-- Module: Mathlib.Analysis.Normed.Field.Dense
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'
pos : ∀ (hS : S.Nonempty), δ ≤ ‖a - a'‖
neg : ∀ (hS : ¬S.Nonempty), δ ≤ ‖a - a'‖
⊢ δ ≤ ‖a - a'‖

Tactic:
by_cases hS : S.Nonempty

Premises used: Finset.Nonempty
-- Module: Mathlib.Analysis.Normed.Field.Dense
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
pos : Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ ≤ ‖a - a'‖
⊢ δ ≤ ‖a - a'‖

Tactic:
simp only [hS, ↓reduceDIte, δ]

Premises used: reduceDIte
-- Module: Mathlib.Analysis.Normed.Field.Dense
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
neg : 1 ≤ ‖a - a'‖
⊢ δ ≤ ‖a - a'‖

Tactic:
simp only [hS, ↓reduceDIte, δ]

Premises used: reduceDIte
-- Module: Mathlib.Analysis.Normed.Field.Dense
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
pos : Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ‖a - a'‖
⊢ Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ ≤ ‖a - a'‖

Tactic:
apply Finset.min'_le (S.image fun x => ‖a - x‖) (‖a - a'‖)

Premises used: Norm.norm, Finset.min'_le, HSub.hSub, Finset.image
-- Module: Mathlib.Analysis.Normed.Field.Dense
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
pos : a' ∈ S
⊢ Membership.mem (γ := Finset ℝ) (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ‖a - a'‖

Tactic:
apply Finset.mem_image_of_mem

Premises used: Finset.mem_image_of_mem
-- Module: Mathlib.Analysis.Normed.Field.Dense
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
pos : a' ∈ rootSet (minpoly L a) F ∧ a' ≠ a
⊢ a' ∈ S

Tactic:
simp only [minpoly.eq_of_irreducible_of_monic firr fa0 fmon, Finset.mem_filter,
        Set.mem_toFinset, S]

Premises used: minpoly.eq_of_irreducible_of_monic, Finset.mem_filter, Set.mem_toFinset
-- Module: Mathlib.Analysis.Normed.Field.Dense
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
pos : IsConjRoot L a a' ∧ a' ≠ a
⊢ a' ∈ rootSet (minpoly L a) F ∧ a' ≠ a

Tactic:
rw [← (isConjRoot_iff_mem_minpoly_rootSet ⟨f, fmon, fa0⟩)]

Premises used: isConjRoot_iff_mem_minpoly_rootSet, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Field.Dense
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
⊢ IsConjRoot L a a' ∧ a' ≠ a

Tactic:
⟨conj, ne.symm⟩

Premises used: Ne.symm, And.intro
-- Module: Mathlib.Analysis.Normed.Field.Dense
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
⊢ IsConjRoot L a a' ∧ a' ≠ a

Tactic:
exact ⟨conj, ne.symm⟩
-- Module: Mathlib.Analysis.Normed.Field.Dense
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
⊢ ∀ ⦃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

Premises used: Classical.not_not, Finset.not_nonempty_iff_eq_empty, ne_eq, Finset.filter_eq_empty_iff, Set.mem_toFinset
-- Module: Mathlib.Analysis.Normed.Field.Dense
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
⊢ 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

Premises used: isConjRoot_iff_mem_minpoly_rootSet, minpoly.eq_of_irreducible_of_monic, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Field.Dense
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
conj₁ : Membership.mem (γ := Set f.SplittingField) (f.rootSet f.SplittingField) a'
⊢ a ≠ a'

Tactic:
rw [isConjRoot_iff_mem_minpoly_rootSet ⟨f, fmon, fa0⟩,
          ← minpoly.eq_of_irreducible_of_monic firr fa0 fmon] at conj

Premises used: isConjRoot_iff_mem_minpoly_rootSet, minpoly.eq_of_irreducible_of_monic, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Field.Dense
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
conj₁ : Membership.mem (γ := Set f.SplittingField) (f.rootSet f.SplittingField) a'
ne₁ : a ≠ a'
⊢ ∀ ⦃x : F⦄, x ∈ f.rootSet F → x = a

Tactic:
rw [isConjRoot_iff_mem_minpoly_rootSet ⟨f, fmon, fa0⟩,
          ← minpoly.eq_of_irreducible_of_monic firr fa0 fmon] at conj

Premises used: isConjRoot_iff_mem_minpoly_rootSet, minpoly.eq_of_irreducible_of_monic, And.intro, Exists.intro