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_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

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⟩
-- 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‖ < δ
bbot : Membership.mem (γ := IntermediateField L F) ⊥ b
⊢ ¬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

Premises used: Polynomial.IsRoot.def, ne_eq, Polynomial.mem_roots', Polynomial.eval_map_algebraMap, Polynomial.map_eq_zero
-- 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‖ < δ
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
⊢ (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)
-- 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‖ < δ
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
masp : (map (algebraMap L F) (minpoly L a)).Splits
⊢ Membership.mem (γ := IntermediateField L F) ⊥ a

Tactic:
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)

Premises used: Iff.mpr, IntermediateField.adjoin_simple_eq_bot_iff, And.right, Irreducible.separable, And.intro, Exists.intro, Polynomial.map, Polynomial.Monic.map, minpoly.irreducible, IsKrasner.krasner, lt_of_lt_of_le
-- 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‖ < δ
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

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)
-- 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‖ < δ
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
H : ∀ (aCp : L) (haCp : (algebraMap L f.SplittingField : (a : L) → f.SplittingField) aCp = a), ∃ (x : L), eval x f = 0
⊢ ∃ (x : L), eval x f = 0

Tactic:
obtain ⟨aCp, haCp⟩ := IntermediateField.mem_bot.mp abot

Premises used: Iff.mp, 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‖ < δ
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
aCp : L
haCp : (algebraMap L f.SplittingField : (a : L) → f.SplittingField) aCp = a
h : eval aCp f = 0
⊢ ∃ (x : L), eval x f = 0

Tactic:
use aCp
-- 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‖ < δ
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
aCp : L
haCp : (algebraMap L f.SplittingField : (a : L) → f.SplittingField) aCp = a
h : Eq (α := F) ((algebraMap L F : (a : L) → F) (eval aCp f) : F) ((algebraMap L F : (a : L) → F) 0 : F)
h₁ : Function.Injective (α := L) (β := F) (⇑(algebraMap L F) : (a : L) → F)
⊢ eval aCp f = 0

Tactic:
apply_fun algebraMap L F

Premises used: Algebra.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 ⋯ ⋯
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
aCp : L
haCp : (algebraMap L f.SplittingField : (a : L) → f.SplittingField) aCp = a
h :
  Eq (α := F) (((aeval ((algebraMap L F : (a : L) → F) aCp) : L[X] →ₐ[L] F) : (a : L[X]) → F) f : F)
    ((algebraMap L F : (a : L) → F) 0 : F)
h₁ : Eq (α := F) ((aeval a : (a : L[X]) → F) f : F) ((algebraMap L F : (a : L) → F) 0 : F)
h₂ h₃ h₄ h₅ : Eq (α := F) ((aeval a : (a : L[X]) → F) f : F) (0 : F)
⊢ Eq (α := F) ((algebraMap L F : (a : L) → F) (eval aCp f) : F) ((algebraMap L F : (a : L) → F) 0 : F)

Tactic:
rwa [← Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval, haCp, map_zero]

Premises used: Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval, map_zero
-- 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‖ < δ
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
aCp : L
haCp : (algebraMap L f.SplittingField : (a : L) → f.SplittingField) aCp = a
⊢ Function.Injective (α := L) (β := F) (⇑(algebraMap L F) : (a : L) → F)

Tactic:
RingHom.injective _

Premises used: RingHom.injective
-- 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‖ < δ
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
aCp : L
haCp : (algebraMap L f.SplittingField : (a : L) → f.SplittingField) aCp = a
⊢ Function.Injective (α := L) (β := F) (⇑(algebraMap L F) : (a : L) → F)

Tactic:
exact RingHom.injective _

Premises used: RingHom.injective
-- Module: Mathlib.Analysis.Normed.Field.Instances
Goal:
F : Type u_1
inst : NormedField F
f : Filter F
hc : Cauchy f
hn : nhds 0 ⊓ f = ⊥
obtain : ∀ (δ : ℝ) (δ_pos : δ > 0) (hδ : ∀ᶠ (y : F) in f, δ ≤ ‖y‖), Cauchy (α := F) (map (fun (x : F) ↦ x⁻¹) f)
⊢ Cauchy (α := F) (map (fun (x : F) ↦ x⁻¹) f)

Tactic:
obtain ⟨δ, δ_pos, hδ⟩ := (disjoint_nhds_zero ..).mp <| disjoint_iff.mpr hn

Premises used: Iff.mpr, SeminormedAddGroup.disjoint_nhds_zero, disjoint_iff, Iff.mp
-- Module: Mathlib.Analysis.Normed.Field.Instances
Goal:
F : Type u_1
inst : NormedField F
f : Filter F
hc : Cauchy f
hn : nhds 0 ⊓ f = ⊥
δ : ℝ
δ_pos : δ > 0
hδ : ∀ᶠ (y : F) in f, δ ≤ ‖y‖
y : F
hy : δ ≤ ‖y‖
⊢ δ ≤ ((fun (x : F) ↦ ‖x⁻¹‖) y)⁻¹

Tactic:
simpa using hy
-- Module: Mathlib.Analysis.Normed.Field.Instances
Goal:
F : Type u_1
inst : NormedField F
f : Filter F
hc : Cauchy f
hn : nhds 0 ⊓ f = ⊥
δ : ℝ
δ_pos : δ > 0
hδ : ∀ᶠ (y : F) in f, δ ≤ ‖y‖
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : F) ↦ ‖x⁻¹‖

Tactic:
have f_bdd : f.IsBoundedUnder (· ≤ ·) (‖·⁻¹‖) :=
      ⟨δ⁻¹, hδ.mono fun y hy ↦ le_inv_of_le_inv₀ δ_pos (by simpa using hy)⟩
-- Module: Mathlib.Analysis.Normed.Field.Instances
Goal:
F : Type u_1
inst : NormedField F
f : Filter F
hc : Cauchy f
hn : nhds 0 ⊓ f = ⊥
δ : ℝ
δ_pos : δ > 0
hδ : ∀ᶠ (y : F) in f, δ ≤ ‖y‖
f_bdd : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : F) ↦ ‖x⁻¹‖
y : F
hy : δ ≤ ‖y‖
⊢ y ≠ 0

Tactic:
simpa using δ_pos.trans_le hy

Premises used: LT.lt.trans_le
-- Module: Mathlib.Analysis.Normed.Field.Instances
Goal:
F : Type u_1
inst : NormedField F
f : Filter F
hc : Cauchy f
hn : nhds 0 ⊓ f = ⊥
δ : ℝ
δ_pos : δ > 0
hδ : ∀ᶠ (y : F) in f, δ ≤ ‖y‖
f_bdd : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : F) ↦ ‖x⁻¹‖
⊢ ∀ᶠ (y : F) in f, y ≠ 0

Tactic:
have h₀ : ∀ᶠ y in f, y ≠ 0 := hδ.mono fun y hy ↦ by simpa using δ_pos.trans_le hy