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
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
⊢ ∃ (x : L), eval x f = 0
have h : eval aCp f = 0
Tactic: use aCp
-- 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
aCp : L
haCp : (algebraMap L f.SplittingField : (a : L) → f.SplittingField) aCp = a
⊢ eval aCp f = 0
have h : Eq (α := F) ((algebraMap L F : (a : L) → F) (eval aCp f) : F) ((algebraMap L F : (a : L) → F) 0 : F)
Tactic: apply_fun algebraMap L F
-- 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
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)
⊢ eval aCp f = 0
have h₁ : Function.Injective (α := L) (β := F) (⇑(algebraMap L F) : (a : L) → F)
Tactic: apply_fun algebraMap L F
-- 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
aCp : L
haCp : (algebraMap L f.SplittingField : (a : L) → f.SplittingField) aCp = a
⊢ Eq (α := F) ((algebraMap L F : (a : L) → F) (eval aCp f) : F) ((algebraMap L F : (a : L) → F) 0 : F)
have 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)
Tactic: rwa [← Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval, haCp, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Dense (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : NontriviallyNormedField L
inst_2 : CompleteSpace L
inst_3 : CharZero L
inst_4 : IsUltrametricDist L
inst_5 : Algebra K L
hi : DenseRange.{u_2, u_1} (X := L) (α := K) (⇑(algebraMap K L) : (a : K) → L)
inst_6 : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this_1 : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : Eq (α := f.SplittingField) ((aeval a : (a : L[X]) → f.SplittingField) f) 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then Finset.min' (Finset.image (fun (x : f.SplittingField) ↦ ‖a - x‖) S) ⋯ else 1
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
δ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)
⊢ Eq (α := F) ((algebraMap L F : (a : L) → F) (eval aCp f) : F) ((algebraMap L F : (a : L) → F) 0 : F)
have h₁ : Eq (α := F) ((aeval a : (a : L[X]) → F) f : F) ((algebraMap L F : (a : L) → F) 0 : F)
Tactic: rwa [← Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval, haCp, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Instances (goal)
Goal:
F : Type u_1
inst : NormedField F
f : Filter F
hc : Cauchy f
hn : nhds 0 ⊓ f = ⊥
⊢ Cauchy (α := F) (map (fun (x : F) ↦ x⁻¹) f)
have obtain : ∀ (δ : ℝ) (δ_pos : δ > 0) (hδ : ∀ᶠ (y : F) in f, δ ≤ ‖y‖), Cauchy (α := F) (map (fun (x : F) ↦ x⁻¹) f)
Tactic: obtain ⟨δ, δ_pos, hδ⟩ := (disjoint_nhds_zero ..).mp <| disjoint_iff.mpr hn
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Instances (hypothesis)
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‖
⊢ Cauchy (α := F) (map (fun (x : F) ↦ x⁻¹) f)
have f_bdd : 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)⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Instances (hypothesis)
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⁻¹‖
⊢ Cauchy (α := F) (map (fun (x : F) ↦ x⁻¹) f)
have h₀ : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Instances (hypothesis)
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⁻¹‖
h₀ : ∀ᶠ (y : F) in f, y ≠ 0
⊢ Cauchy (α := F) (map (fun (x : F) ↦ x⁻¹) f)
have this : ∀ᶠ (p : F × F) in f ×ˢ f, p.1⁻¹ - p.2⁻¹ = p.1⁻¹ * (p.2 - p.1) * p.2⁻¹
Tactic: have : ∀ᶠ p in f ×ˢ f, p.1⁻¹ - p.2⁻¹ = p.1⁻¹ * (p.2 - p.1) * p.2⁻¹ :=
      h₀.prod_mk h₀ |>.mono fun ⟨x, y⟩ ⟨hx, hy⟩ ↦ by simp [mul_sub, sub_mul, hx, hy]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Instances (goal)
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⁻¹‖
h₀ : ∀ᶠ (y : F) in f, y ≠ 0
this : ∀ᶠ (p : F × F) in f ×ˢ f, p.1⁻¹ - p.2⁻¹ = p.1⁻¹ * (p.2 - p.1) * p.2⁻¹
⊢ Cauchy (α := F) (map (fun (x : F) ↦ x⁻¹) f)
have rw : ∀ (hc : f.NeBot ∧ Tendsto (β := F) (fun (p : F × F) ↦ p.2 - p.1) (f ×ˢ f) (nhds 0)) (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⁻¹‖) (h₀ : ∀ᶠ (y : F) in f, y ≠ 0)
  (this : ∀ᶠ (p : F × F) in f ×ˢ f, p.1⁻¹ - p.2⁻¹ = p.1⁻¹ * (p.2 - p.1) * p.2⁻¹),
  Cauchy (α := F) (map (fun (x : F) ↦ x⁻¹) f)
Tactic: rw [cauchy_iff_tendsto_swapped] at hc
Cleared hypotheses: hc, hn, δ, δ_pos, hδ, f_bdd, h₀, this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Instances (goal)
Goal:
F : Type u_1
inst : NormedField F
f : Filter F
hc : f.NeBot ∧ Tendsto (β := F) (fun (p : F × F) ↦ p.2 - p.1) (f ×ˢ f) (nhds 0)
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⁻¹‖
h₀ : ∀ᶠ (y : F) in f, y ≠ 0
this : ∀ᶠ (p : F × F) in f ×ˢ f, p.1⁻¹ - p.2⁻¹ = p.1⁻¹ * (p.2 - p.1) * p.2⁻¹
⊢ Cauchy (α := F) (map (fun (x : F) ↦ x⁻¹) f)
have rw : f.NeBot ∧ Tendsto (β := F) (fun (x : F × F) ↦ x.1⁻¹ * (x.2 - x.1) * x.2⁻¹) (f ×ˢ f) (nhds 0)
Tactic: rw [cauchy_map_iff_tendsto, tendsto_congr' this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Instances (goal)
Goal:
F : Type u_1
inst : NormedField F
f : Filter F
hc : f.NeBot ∧ Tendsto (β := F) (fun (p : F × F) ↦ p.2 - p.1) (f ×ˢ f) (nhds 0)
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⁻¹‖
h₀ : ∀ᶠ (y : F) in f, y ≠ 0
this : ∀ᶠ (p : F × F) in f ×ˢ f, p.1⁻¹ - p.2⁻¹ = p.1⁻¹ * (p.2 - p.1) * p.2⁻¹
⊢ f.NeBot ∧ Tendsto (β := F) (fun (x : F × F) ↦ x.1⁻¹ * (x.2 - x.1) * x.2⁻¹) (f ×ˢ f) (nhds 0)
have refine : Tendsto (β := F) (fun (x : F × F) ↦ x.1⁻¹ * (x.2 - x.1)) (f ×ˢ f) (nhds 0)
Tactic: refine ⟨hc.1, .zero_mul_isBoundedUnder_le ?_ <| tendsto_snd.isBoundedUnder_comp f_bdd⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
⊢ Membership.mem (γ := IntermediateField K L) K⟮y⟯ x
have this : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
Tactic: have := IntermediateField.adjoin.finiteDimensional yint
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
⊢ Membership.mem (γ := IntermediateField K L) K⟮y⟯ x
have this₁ : IsUltrametricDist L
Tactic: have : IsUltrametricDist L := IsUltrametricDist.of_normedAlgebra K
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
this : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
⊢ Membership.mem (γ := IntermediateField K L) K⟮y⟯ x
have zsep : IsSeparable (↥K⟮y⟯) z
Tactic: have zsep : IsSeparable K⟮y⟯ z :=
      Field.isSeparable_sub (IsSeparable.tower_top K⟮y⟯ xsep) (isSeparable_algebraMap y')
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
this : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
⊢ Membership.mem (γ := IntermediateField K L) K⟮y⟯ x
have suffices : Membership.mem (γ := IntermediateField K L) K⟮y⟯ z
Tactic: suffices z ∈ K⟮y⟯ by simpa [z, y'] using add_mem this y'.2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
this : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
⊢ Membership.mem (γ := IntermediateField K L) K⟮y⟯ z
have this₁ : Membership.mem (γ := IntermediateField K L) K⟮y⟯ z ↔ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z
Tactic: have : z ∈ K⟮y⟯ ↔ z ∈ (⊥ : Subalgebra K⟮y⟯ L) := by simp [Algebra.mem_bot]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
this_2 : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : Membership.mem (γ := IntermediateField K L) K⟮y⟯ z ↔ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z
⊢ Membership.mem (γ := IntermediateField K L) K⟮y⟯ z
have rw : Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
this_2 : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : Membership.mem (γ := IntermediateField K L) K⟮y⟯ z ↔ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z
⊢ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z
have by_contra : ∀ (hz : z ∉ ⊥), False
Tactic: by_contra hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
this_2 : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : Membership.mem (γ := IntermediateField K L) K⟮y⟯ z ↔ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z
hz : z ∉ ⊥
⊢ False
have obtain : ∀ (z' : L) (hne : z ≠ z') (h1 : IsConjRoot (↥K⟮y⟯) z z'), False
Tactic: obtain ⟨z', hne, h1⟩ := (notMem_iff_exists_ne_and_isConjRoot zsep
        (minpoly_sub_algebraMap_splits y' (IsIntegral.minpoly_splits_tower_top
          xsep.isIntegral sp))).mp hz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (goal)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
this_2 : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : Membership.mem (γ := IntermediateField K L) K⟮y⟯ z ↔ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
⊢ False
have obtain : ∀ (σ : Gal(L/↥K⟮y⟯)) (hσ : (σ : (a : L) → L) z' = z), False
Tactic: obtain ⟨σ, hσ⟩ := isConjRoot_iff_exists_algEquiv.mp h1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
this_2 : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : Membership.mem (γ := IntermediateField K L) K⟮y⟯ z ↔ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : (σ : (a : L) → L) z' = z
⊢ False
have hσ₁ : Eq (α := L) ((σ.symm : (a : L) → L) ((σ : (a : L) → L) z' : L) : L) ((σ.symm : (a : L) → L) z : L)
Tactic: apply_fun σ.symm at hσ
Cleared hypotheses: hσ
-- Lean 4 proof step from Mathlib.Analysis.Normed.Field.Krasner (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : NontriviallyNormedField K
inst_2 : CompleteSpace K
inst_3 : IsUltrametricDist K
inst_4 : NormedAlgebra K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : Normal K L
x y : L
xsep : IsSeparable K x
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
yint : IsIntegral K y
kr : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
z : L := x - y
this_1 : FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯
this_2 : IsUltrametricDist L
y' : ↥K⟮y⟯ := AdjoinSimple.gen K y
zsep : IsSeparable (↥K⟮y⟯) z
this : Membership.mem (γ := IntermediateField K L) K⟮y⟯ z ↔ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z
hz : z ∉ ⊥
z' : L
hne : z ≠ z'
h1 : IsConjRoot (↥K⟮y⟯) z z'
σ : Gal(L/↥K⟮y⟯)
hσ : Eq (α := L) ((σ.symm : (a : L) → L) ((σ : (a : L) → L) z' : L) : L) ((σ.symm : (a : L) → L) z : L)
⊢ False
have hσ₁ : z' = (σ.symm : (a : L) → L) z
Tactic: simp only [AlgEquiv.symm_apply_apply] at hσ
Cleared hypotheses: hσ