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
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‖ < δ
have rw : ∀ (hab : ‖a - b‖ < HPow.hPow (β := ℝ) (δ / max ‖a‖ 1) 1 * max ‖a‖ 1), ‖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
Cleared hypotheses: hab
-- 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
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‖ < δ
⊢ ‖a - b‖ < δ
have rw₁ : ∀ (hab : ‖a - b‖ < (δ / max ‖a‖ 1) ^ HMul.hMul (α := ℝ) (↑f.natDegree : ℝ) (↑f.natDegree : ℝ)⁻¹ * max ‖a‖ 1),
  Ne (α := ℝ) (↑f.natDegree : ℝ) 0
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
Cleared hypotheses: hab
-- 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
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
⊢ ‖a - b‖ < δ
have 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
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
Cleared hypotheses: hab
-- 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
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
⊢ ∃ (x : L), eval x f = 0
have hab₁ : ‖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
-- 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
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‖ < δ
⊢ Membership.mem (γ := IntermediateField L F) ⊥ b
have hb₁ : ∃ 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
Cleared hypotheses: hb, hab_1, hab
-- 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
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‖ < δ
⊢ Membership.mem (γ := IntermediateField L F) ⊥ b
have 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
Tactic: obtain ⟨bCp, _, hbCp⟩ := hb
Cleared hypotheses: hb
-- 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
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 (γ := IntermediateField L F) ⊥ b
have rw : Membership.mem (γ := Set f.SplittingField)
  (Set.range (ι := L) (⇑(algebraMap L f.SplittingField) : (a : L) → f.SplittingField)) b
Tactic: rw [IntermediateField.mem_bot]
-- 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
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‖ < δ
⊢ ∃ (x : L), eval x f = 0
have bbot : Membership.mem (γ := IntermediateField L F) ⊥ b
Tactic: have bbot : b ∈ (⊥ : IntermediateField L F) := by
    rw [Polynomial.aroots_def, Splits.roots_map ((IsAlgClosed.splits g).map _),
        Multiset.mem_map] at hb
    obtain ⟨bCp, _, hbCp⟩ := hb
    rw [IntermediateField.mem_bot]
    exact ⟨bCp, hbCp⟩
-- 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
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‖ < δ
bbot : Membership.mem (γ := IntermediateField L F) ⊥ b
⊢ ∃ (x : L), eval x f = 0
have hb₁ : ¬g = 0 ∧ Eq (α := f.SplittingField) ((aeval b : (a : L[X]) → f.SplittingField) (map (algebraMap K L) g)) 0
Tactic: simp only [Polynomial.mem_roots', ne_eq, Polynomial.map_eq_zero, Polynomial.IsRoot.def,
    Polynomial.eval_map_algebraMap] at hb
Cleared hypotheses: hb
-- 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
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‖ < δ
bbot : Membership.mem (γ := IntermediateField L F) ⊥ b
hb : ¬g = 0 ∧ Eq (α := f.SplittingField) ((aeval b : (a : L[X]) → f.SplittingField) (map (algebraMap K L) g)) 0
⊢ Membership.mem (γ := IntermediateField L F) ⊥ a
have masp : (map (algebraMap L F) (minpoly L a)).Splits
Tactic: have masp : ((minpoly L a).map (algebraMap L F)).Splits := by
      simpa [minpoly.eq_of_irreducible_of_monic firr fa0 fmon] using
        (Polynomial.SplittingField.splits f)
-- 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
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‖ < δ
bbot : Membership.mem (γ := IntermediateField L F) ⊥ b
hb : ¬g = 0 ∧ Eq (α := f.SplittingField) ((aeval b : (a : L[X]) → f.SplittingField) (map (algebraMap K L) g)) 0
⊢ ∃ (x : L), eval x f = 0
have abot : Membership.mem (γ := IntermediateField L F) ⊥ a
Tactic: have abot : a ∈ (⊥ : IntermediateField L F) := by
    have masp : ((minpoly L a).map (algebraMap L F)).Splits := by
      simpa [minpoly.eq_of_irreducible_of_monic firr fa0 fmon] using
        (Polynomial.SplittingField.splits f)
    simpa [IntermediateField.adjoin_simple_eq_bot_iff.mpr bbot] using
      IsKrasner.krasner (minpoly.irreducible ⟨f, fmon, fa0⟩).separable
        masp ⟨(g.map _), gmon.map _, hb.2⟩ fun a' h1 h2 ↦ lt_of_lt_of_le hab (norm_sub_le a' h1 h2)
-- 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
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‖ < δ
bbot : Membership.mem (γ := IntermediateField L F) ⊥ b
hb : ¬g = 0 ∧ Eq (α := f.SplittingField) ((aeval b : (a : L[X]) → f.SplittingField) (map (algebraMap K L) g)) 0
abot : Membership.mem (γ := IntermediateField L F) ⊥ a
⊢ ∃ (x : L), eval x f = 0
have H : ∀ (aCp : L) (haCp : (algebraMap L f.SplittingField : (a : L) → f.SplittingField) aCp = a), ∃ (x : L), eval x f = 0
Tactic: obtain ⟨aCp, haCp⟩ := IntermediateField.mem_bot.mp abot