awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
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
rw : ∀ (hab : ‖a - b‖ < HPow.hPow (β := ℝ) (δ / max ‖a‖ 1) 1 * max ‖a‖ 1), ‖a - b‖ < δ
rw₁ :
  ∀ (hab : ‖a - b‖ < (δ / max ‖a‖ 1) ^ HMul.hMul (α := ℝ) (↑f.natDegree : ℝ) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1),
    Ne (α := ℝ) (↑f.natDegree : ℝ) 0
rw₂ :
  ∀
    (hab :
      ‖a - b‖ <
        HPow.hPow (β := ℝ)
            (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 / HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 *
              HPow.hPow (β := ℝ) (δ / max ‖a‖ 1) (↑f.natDegree : ℝ))
            (↑f.natDegree : ℝ)⁻¹ *
          max ‖a‖ 1),
    HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 ≠ 0
⊢ ‖a - b‖ < δ

Tactic:
rw [← Real.rpow_natCast, ← mul_comm_div, div_self, one_mul,
        ← Real.rpow_mul (div_pos δpos (by positivity)).le, mul_inv_cancel₀] at hab

Premises used: mul_inv_cancel₀, LT.lt.le, mul_comm_div, div_pos, Real.rpow_mul, one_mul, div_self, Real.rpow_natCast
-- 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
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
b : f.SplittingField
hb : Membership.mem (γ := Multiset f.SplittingField) (aroots (map (algebraMap K L) g) f.SplittingField) b
hab : ‖a - b‖ < HPow.hPow (β := ℝ) (δ / max ‖a‖ 1) 1 * max ‖a‖ 1
⊢ max ‖a‖ 1 > 0

Tactic:
positivity
-- 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
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
b : f.SplittingField
hb : Membership.mem (γ := Multiset f.SplittingField) (aroots (map (algebraMap K L) g) f.SplittingField) b
hab : ‖a - b‖ < HPow.hPow (β := ℝ) (δ / max ‖a‖ 1) 1 * max ‖a‖ 1
⊢ ‖a - b‖ < δ

Tactic:
simpa [mul_assoc, div_mul_cancel₀ _ (by positivity : (max ‖a‖ 1) > 0).ne'] using hab

Premises used: div_mul_cancel₀, mul_assoc, LT.lt.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 ⋯ ⋯
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
b : f.SplittingField
hb : Membership.mem (γ := Multiset f.SplittingField) (aroots (map (algebraMap K L) g) f.SplittingField) b
hab : ‖a - b‖ < (δ / max ‖a‖ 1) ^ HMul.hMul (α := ℝ) (↑f.natDegree : ℝ) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1
⊢ Ne (α := ℝ) (↑f.natDegree : ℝ) 0

Tactic:
simp [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
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
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 / HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 *
          HPow.hPow (β := ℝ) (δ / max ‖a‖ 1) (↑f.natDegree : ℝ))
        (↑f.natDegree : ℝ)⁻¹ *
      max ‖a‖ 1
⊢ HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 ≠ 0

Tactic:
positivity
-- 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
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
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
⊢ ‖a - b‖ < δ

Tactic:
have hab : ‖a - b‖ < δ := by
    rw [← Real.rpow_natCast, ← mul_comm_div, div_self, one_mul,
        ← Real.rpow_mul (div_pos δpos (by positivity)).le, mul_inv_cancel₀] at hab
    · simpa [mul_assoc, div_mul_cancel₀ _ (by positivity : (max ‖a‖ 1) > 0).ne'] using hab
    · simp [fnatdeg0]
    · positivity
-- 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
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
b : f.SplittingField
hb : Membership.mem (γ := Multiset f.SplittingField) (aroots (map (algebraMap K L) g) f.SplittingField) b
hab_1 :
  ‖a - b‖ <
    HPow.hPow (β := ℝ)
        (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 *
          ((δ / max ‖a‖ 1) ^ f.natDegree / HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1))
        (↑f.natDegree : ℝ)⁻¹ *
      max ‖a‖ 1
hab : ‖a - b‖ < δ
⊢ ∃ a ∈ roots (map (algebraMap K L) g), (algebraMap L f.SplittingField : (a : L) → f.SplittingField) a = b

Tactic:
rw [Polynomial.aroots_def, Splits.roots_map ((IsAlgClosed.splits g).map _),
        Multiset.mem_map] at hb

Premises used: Multiset.mem_map, Polynomial.Splits.roots_map, IsAlgClosed.splits, Polynomial.Splits.map, Polynomial.aroots_def
-- 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
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
b : f.SplittingField
hb : Membership.mem (γ := Multiset f.SplittingField) (aroots (map (algebraMap K L) g) f.SplittingField) b
hab_1 :
  ‖a - b‖ <
    HPow.hPow (β := ℝ)
        (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 *
          ((δ / max ‖a‖ 1) ^ f.natDegree / HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1))
        (↑f.natDegree : ℝ)⁻¹ *
      max ‖a‖ 1
hab : ‖a - b‖ < δ
hb₁ : ∃ a ∈ roots (map (algebraMap K L) g), (algebraMap L f.SplittingField : (a : L) → f.SplittingField) a = b
⊢ ‖a - b‖ <
    HPow.hPow (β := ℝ)
        (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 *
          ((δ / max ‖a‖ 1) ^ f.natDegree / HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1))
        (↑f.natDegree : ℝ)⁻¹ *
      max ‖a‖ 1

Tactic:
rw [Polynomial.aroots_def, Splits.roots_map ((IsAlgClosed.splits g).map _),
        Multiset.mem_map] at hb

Premises used: Multiset.mem_map, Polynomial.Splits.roots_map, IsAlgClosed.splits, Polynomial.Splits.map, Polynomial.aroots_def
-- 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
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
b : f.SplittingField
hb : Membership.mem (γ := Multiset f.SplittingField) (aroots (map (algebraMap K L) g) f.SplittingField) b
hab_1 :
  ‖a - b‖ <
    HPow.hPow (β := ℝ)
        (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 *
          ((δ / max ‖a‖ 1) ^ f.natDegree / HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1))
        (↑f.natDegree : ℝ)⁻¹ *
      max ‖a‖ 1
hab : ‖a - b‖ < δ
hb₁ : ∃ a ∈ roots (map (algebraMap K L) g), (algebraMap L f.SplittingField : (a : L) → f.SplittingField) a = 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
⊢ ‖a - b‖ < δ

Tactic:
rw [Polynomial.aroots_def, Splits.roots_map ((IsAlgClosed.splits g).map _),
        Multiset.mem_map] at hb

Premises used: Multiset.mem_map, Polynomial.Splits.roots_map, IsAlgClosed.splits, Polynomial.Splits.map, Polynomial.aroots_def
-- 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
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
b : f.SplittingField
hb : ∃ a ∈ roots (map (algebraMap K L) g), (algebraMap L f.SplittingField : (a : L) → f.SplittingField) a = b
hab_1 :
  ‖a - b‖ <
    HPow.hPow (β := ℝ)
        (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 *
          ((δ / max ‖a‖ 1) ^ f.natDegree / HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1))
        (↑f.natDegree : ℝ)⁻¹ *
      max ‖a‖ 1
hab : ‖a - b‖ < δ
obtain :
  ∀ bCp ∈ roots (map (algebraMap K L) g),
    ∀ (hbCp : (algebraMap L f.SplittingField : (a : L) → f.SplittingField) bCp = b),
      Membership.mem (γ := IntermediateField L F) ⊥ b
⊢ Membership.mem (γ := IntermediateField L F) ⊥ b

Tactic:
obtain ⟨bCp, _, hbCp⟩ := hb
-- 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
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
b : f.SplittingField
hab_1 :
  ‖a - b‖ <
    HPow.hPow (β := ℝ)
        (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 *
          ((δ / max ‖a‖ 1) ^ f.natDegree / HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1))
        (↑f.natDegree : ℝ)⁻¹ *
      max ‖a‖ 1
hab : ‖a - b‖ < δ
bCp : L
left : bCp ∈ roots (map (algebraMap K L) g)
hbCp : (algebraMap L f.SplittingField : (a : L) → f.SplittingField) bCp = b
rw :
  Membership.mem (γ := Set f.SplittingField)
    (Set.range (ι := L) (⇑(algebraMap L f.SplittingField) : (a : L) → f.SplittingField)) b
⊢ Membership.mem (γ := IntermediateField L F) ⊥ b

Tactic:
rw [IntermediateField.mem_bot]

Premises used: IntermediateField.mem_bot
-- 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
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
b : f.SplittingField
hab_1 :
  ‖a - b‖ <
    HPow.hPow (β := ℝ)
        (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 *
          ((δ / max ‖a‖ 1) ^ f.natDegree / HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1))
        (↑f.natDegree : ℝ)⁻¹ *
      max ‖a‖ 1
hab : ‖a - b‖ < δ
bCp : L
left : bCp ∈ roots (map (algebraMap K L) g)
hbCp : (algebraMap L f.SplittingField : (a : L) → f.SplittingField) bCp = b
⊢ Membership.mem (γ := Set f.SplittingField)
    (Set.range (ι := L) (⇑(algebraMap L f.SplittingField) : (a : L) → f.SplittingField)) b

Tactic:
⟨bCp, hbCp⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range
-- 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
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
b : f.SplittingField
hab_1 :
  ‖a - b‖ <
    HPow.hPow (β := ℝ)
        (HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1 *
          ((δ / max ‖a‖ 1) ^ f.natDegree / HAdd.hAdd (α := ℝ) (↑f.natDegree : ℝ) 1))
        (↑f.natDegree : ℝ)⁻¹ *
      max ‖a‖ 1
hab : ‖a - b‖ < δ
bCp : L
left : bCp ∈ roots (map (algebraMap K L) g)
hbCp : (algebraMap L f.SplittingField : (a : L) → f.SplittingField) bCp = b
⊢ Membership.mem (γ := Set f.SplittingField)
    (Set.range (ι := L) (⇑(algebraMap L f.SplittingField) : (a : L) → f.SplittingField)) b

Tactic:
exact ⟨bCp, hbCp⟩