awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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⁻¹‖
h₀ : ∀ᶠ (y : F) in f, y ≠ 0
x_1 : F × F
x y : F
h : (x, y).1 ≠ 0 ∧ (x, y).2 ≠ 0
hx : (x, y).1 ≠ 0
hy : (x, y).2 ≠ 0
⊢ (x, y).1⁻¹ - (x, y).2⁻¹ = (x, y).1⁻¹ * ((x, y).2 - (x, y).1) * (x, y).2⁻¹

Tactic:
simp [mul_sub, sub_mul, hx, hy]

Premises used: mul_sub, sub_mul
-- 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⁻¹‖
h₀ : ∀ᶠ (y : F) in f, y ≠ 0
⊢ ∀ᶠ (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]
-- 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⁻¹‖
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⁻¹
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)
⊢ Cauchy (α := F) (map (fun (x : F) ↦ x⁻¹) f)

Tactic:
rw [cauchy_iff_tendsto_swapped] at hc

Premises used: IsUniformAddGroup.cauchy_iff_tendsto_swapped
-- Module: Mathlib.Analysis.Normed.Field.Instances
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⁻¹
rw : f.NeBot ∧ Tendsto (β := F) (fun (x : F × F) ↦ x.1⁻¹ * (x.2 - x.1) * x.2⁻¹) (f ×ˢ f) (nhds 0)
⊢ Cauchy (α := F) (map (fun (x : F) ↦ x⁻¹) f)

Tactic:
rw [cauchy_map_iff_tendsto, tendsto_congr' this]

Premises used: IsUniformAddGroup.cauchy_map_iff_tendsto, Filter.tendsto_congr'
-- Module: Mathlib.Analysis.Normed.Field.Instances
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)

Tactic:
⟨hc.1, .zero_mul_isBoundedUnder_le ?_ <| tendsto_snd.isBoundedUnder_comp f_bdd⟩

Premises used: Filter.Tendsto.zero_mul_isBoundedUnder_le, And.left, And.intro, Filter.Tendsto.isBoundedUnder_comp, Filter.tendsto_snd
-- Module: Mathlib.Analysis.Normed.Field.Instances
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⁻¹
refine : Tendsto (β := F) (fun (x : F × F) ↦ x.1⁻¹ * (x.2 - x.1)) (f ×ˢ f) (nhds 0)
⊢ f.NeBot ∧ Tendsto (β := F) (fun (x : F × F) ↦ x.1⁻¹ * (x.2 - x.1) * x.2⁻¹) (f ×ˢ f) (nhds 0)

Tactic:
refine ⟨hc.1, .zero_mul_isBoundedUnder_le ?_ <| tendsto_snd.isBoundedUnder_comp f_bdd⟩
-- Module: Mathlib.Analysis.Normed.Field.Instances
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⁻¹
⊢ Tendsto (β := F) (fun (x : F × F) ↦ x.1⁻¹ * (x.2 - x.1)) (f ×ˢ f) (nhds 0)

Tactic:
isBoundedUnder_le_mul_tendsto_zero (tendsto_fst.isBoundedUnder_comp f_bdd) hc.2

Premises used: Filter.isBoundedUnder_le_mul_tendsto_zero, And.right, Filter.Tendsto.isBoundedUnder_comp, Filter.tendsto_fst
-- Module: Mathlib.Analysis.Normed.Field.Instances
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⁻¹
⊢ Tendsto (β := F) (fun (x : F × F) ↦ x.1⁻¹ * (x.2 - x.1)) (f ×ˢ f) (nhds 0)

Tactic:
exact isBoundedUnder_le_mul_tendsto_zero (tendsto_fst.isBoundedUnder_comp f_bdd) hc.2

Premises used: Filter.isBoundedUnder_le_mul_tendsto_zero, And.right, Filter.Tendsto.isBoundedUnder_comp, Filter.tendsto_fst
-- Module: Mathlib.Analysis.Normed.Field.Krasner
Goal:
K : Type u_1
L : Type u_2
inst : NormedField L
inst_1 : Field K
inst_2 : Algebra K L
inst_3 : IsKrasner K L
x y : L
hx : Polynomial.Separable (minpoly K x)
sp : Polynomial.Splits (Polynomial.map (algebraMap K L) (minpoly K x))
hy : IsIntegral K y
h : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖
⊢ Membership.mem (γ := IntermediateField K L) K⟮y⟯ x

Tactic:
IsKrasner.krasner' hx sp hy h

Premises used: IsKrasner.krasner'
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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
⊢ FiniteDimensional.{u_1, u_2} K ↥K⟮y⟯

Tactic:
have := IntermediateField.adjoin.finiteDimensional yint
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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⟯
⊢ IsUltrametricDist L

Tactic:
have : IsUltrametricDist L := IsUltrametricDist.of_normedAlgebra K
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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
⊢ IsSeparable (↥K⟮y⟯) z

Tactic:
have zsep : IsSeparable K⟮y⟯ z :=
      Field.isSeparable_sub (IsSeparable.tower_top K⟮y⟯ xsep) (isSeparable_algebraMap y')
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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 (γ := IntermediateField K L) K⟮y⟯ x

Tactic:
simpa [z, y'] using add_mem this y'.2

Premises used: AddMemClass.add_mem, Subtype.property
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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
suffices : Membership.mem (γ := IntermediateField K L) K⟮y⟯ z
⊢ Membership.mem (γ := IntermediateField K L) K⟮y⟯ x

Tactic:
suffices z ∈ K⟮y⟯ by simpa [z, y'] using add_mem this y'.2
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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 ↔ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z

Tactic:
simp [Algebra.mem_bot]

Premises used: Algebra.mem_bot
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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 ↔ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z

Tactic:
have : z ∈ K⟮y⟯ ↔ z ∈ (⊥ : Subalgebra K⟮y⟯ L) := by simp [Algebra.mem_bot]
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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
rw : Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z
⊢ Membership.mem (γ := IntermediateField K L) K⟮y⟯ z

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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
by_contra : ∀ (hz : z ∉ ⊥), False
⊢ Membership.mem (γ := Subalgebra (↥K⟮y⟯) L) ⊥ z

Tactic:
by_contra hz
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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 ∉ ⊥
obtain : ∀ (z' : L) (hne : z ≠ z') (h1 : IsConjRoot (↥K⟮y⟯) z z'), False
⊢ 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

Premises used: minpoly_sub_algebraMap_splits, Iff.mp, IsIntegral.minpoly_splits_tower_top, notMem_iff_exists_ne_and_isConjRoot, IsSeparable.isIntegral
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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'
obtain : ∀ (σ : Gal(L/↥K⟮y⟯)) (hσ : (σ : (a : L) → L) z' = z), False
⊢ False

Tactic:
obtain ⟨σ, hσ⟩ := isConjRoot_iff_exists_algEquiv.mp h1

Premises used: isConjRoot_iff_exists_algEquiv, Iff.mp
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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
⊢ Eq (α := L) ((σ.symm : (a : L) → L) ((σ : (a : L) → L) z' : L) : L) ((σ.symm : (a : L) → L) z : L)

Tactic:
apply_fun σ.symm at hσ

Premises used: AlgEquiv.symm
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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)
⊢ z' = (σ.symm : (a : L) → L) z

Tactic:
simp only [AlgEquiv.symm_apply_apply] at hσ

Premises used: AlgEquiv.symm_apply_apply
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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σ : z' = (σ.symm : (a : L) → L) z
⊢ ‖z - z'‖ ≤ max ‖z‖ ‖z'‖

Tactic:
simpa [norm_neg, sub_eq_add_neg] using (IsUltrametricDist.norm_add_le_max z (- z'))

Premises used: sub_eq_add_neg, IsUltrametricDist.norm_add_le_max, norm_neg, Neg.neg
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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σ : z' = (σ.symm : (a : L) → L) z
simp :
  spectralNorm K L z ≤ spectralNorm K L (x - y) ∧
    spectralNorm K L ((σ.symm : (a : L) → L) z : L) ≤ spectralNorm K L (x - y)
⊢ max ‖z‖ ‖z'‖ ≤ ‖x - y‖

Tactic:
simp only [NormedAlgebra.norm_eq_spectralNorm K, hσ, sup_le_iff]

Premises used: NormedAlgebra.norm_eq_spectralNorm, sup_le_iff
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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σ : z' = (σ.symm : (a : L) → L) z
rw : spectralNorm K L z ≤ spectralNorm K L (x - y) ∧ spectralNorm K L z ≤ spectralNorm K L (x - y)
⊢ spectralNorm K L z ≤ spectralNorm K L (x - y) ∧
    spectralNorm K L ((σ.symm : (a : L) → L) z : L) ≤ spectralNorm K L (x - y)

Tactic:
rw [← AlgEquiv.restrictScalars_apply K,
              ← spectralNorm_eq_of_equiv (σ.symm.restrictScalars K)]

Premises used: AlgEquiv.symm, AlgEquiv.restrictScalars, AlgEquiv.restrictScalars_apply, spectralNorm_eq_of_equiv
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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σ : z' = (σ.symm : (a : L) → L) z
⊢ spectralNorm K L z ≤ spectralNorm K L (x - y) ∧ spectralNorm K L z ≤ spectralNorm K L (x - y)

Tactic:
simp [z]
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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σ : z' = (σ.symm : (a : L) → L) z
a : IsConjRoot K x (z' + y)
a₁ : x ≠ z' + y
⊢ ‖x - y‖ < ‖x - (z' + y)‖

Tactic:
apply kr (z' + y)

Premises used: HAdd.hAdd
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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σ : z' = (σ.symm : (a : L) → L) z
a : IsConjRoot (↥K⟮y⟯) x (z' + y)
⊢ IsConjRoot K x (z' + y)

Tactic:
apply IsConjRoot.of_isScalarTower (L := K⟮y⟯) xsep.isIntegral

Premises used: IsConjRoot.of_isScalarTower, IsSeparable.isIntegral
-- Module: Mathlib.Analysis.Normed.Field.Krasner
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σ : z' = (σ.symm : (a : L) → L) z
⊢ IsConjRoot (↥K⟮y⟯) x (z' + y)

Tactic:
simpa [z, y'] using IsConjRoot.add_algebraMap y' h1

Premises used: IsConjRoot.add_algebraMap