awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ x ≠ z' + y

Tactic:
simpa [z, sub_eq_iff_eq_add] using hne

Premises used: sub_eq_iff_eq_add
-- 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
e_a : x - (z' + y) = z - z'
⊢ ‖x - (z' + y)‖ = ‖z - z'‖

Tactic:
congr 1
-- 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
⊢ x - (z' + y) = z - z'

Tactic:
ring
-- 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'‖ < ‖z - z'‖

Tactic:
have : ‖z - z'‖ < ‖z - z'‖ :=
      calc
        _ ≤ max ‖z‖ ‖z'‖ := by
          simpa [norm_neg, sub_eq_add_neg] using (IsUltrametricDist.norm_add_le_max z (- z'))
        _ ≤ ‖x - y‖ := by
          simp only [NormedAlgebra.norm_eq_spectralNorm K, hσ, sup_le_iff]
          rw [← AlgEquiv.restrictScalars_apply K,
              ← spectralNorm_eq_of_equiv (σ.symm.restrictScalars K)]
          simp [z]
        _ < ‖x - (z' + y)‖ := by
          apply kr (z' + y)
          · apply IsConjRoot.of_isScalarTower (L := K⟮y⟯) xsep.isIntegral
            simpa [z, y'] using IsConjRoot.add_algebraMap y' h1
          · simpa [z, sub_eq_iff_eq_add] using hne
        _ = ‖z - z'‖ := by congr 1; ring
-- 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_3 : 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
this : ‖z - z'‖ < ‖z - z'‖
⊢ False

Tactic:
simp [lt_self_iff_false] at this

Premises used: lt_self_iff_false
-- 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
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'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
⊢ ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖

Tactic:
have norm_iL (x : L) : ‖iL x‖ = ‖x‖ := norm_algebraMap' _ _
-- 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
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'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this_4 : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
this : Membership.mem (α := C) (γ := IntermediateField K C) K⟮((iL : (a : L) → C) y : C)⟯ ((iL : (a : L) → C) x : C)
⊢ Membership.mem (γ := IntermediateField K L) K⟮y⟯ x

Tactic:
simpa [← Set.image_singleton, ← IntermediateField.adjoin_map] using this

Premises used: Set.image_singleton, IntermediateField.adjoin_map
-- 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
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'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
suffices : Membership.mem (α := C) (γ := IntermediateField K C) K⟮((iL : (a : L) → C) y : C)⟯ ((iL : (a : L) → C) x : C)
⊢ Membership.mem (γ := IntermediateField K L) K⟮y⟯ x

Tactic:
suffices this : iL x ∈ K⟮iL y⟯ by
      simpa [← Set.image_singleton, ← IntermediateField.adjoin_map] using 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
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'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
⊢ Membership.mem (α := C) (γ := IntermediateField K C) K⟮((iL : (a : L) → C) y : C)⟯ ((iL : (a : L) → C) x : C)

Tactic:
IsKrasner.krasner ((xsep.map _ iL.injective).of_dvd dvd_rfl) ?_ (yint.map iL) ?_

Premises used: IsSeparable.map, Set.Mem, setOf, RingHom.injective, IsIntegral.map, AlgHom.toRingHom, dvd_rfl, Polynomial.Separable.of_dvd, 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
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'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
refine_1 : (Polynomial.map (algebraMap K C) (minpoly K (B := C) ((iL : (a : L) → C) x : C))).Splits
refine_2 :
  ∀ (x' : C),
    IsConjRoot K ((iL : (a : L) → C) x) x' →
      (iL : (a : L) → C) x ≠ x' →
        ‖HSub.hSub (α := C) (β := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) y : C)‖ <
          ‖HSub.hSub (α := C) ((iL : (a : L) → C) x : C) x'‖
⊢ Membership.mem (α := C) (γ := IntermediateField K C) K⟮((iL : (a : L) → C) y : C)⟯ ((iL : (a : L) → C) x : C)

Tactic:
refine IsKrasner.krasner ((xsep.map _ iL.injective).of_dvd dvd_rfl) ?_ (yint.map iL) ?_

Premises used: IsSeparable.map, RingHom.injective, IsIntegral.map, AlgHom.toRingHom, dvd_rfl, Polynomial.Separable.of_dvd, 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
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'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
⊢ Dvd.dvd (α := Polynomial K) (minpoly K (B := C) ((iL : (a : L) → C) x : C)) (minpoly K x)

Tactic:
simpa using minpoly.dvd_map_of_isScalarTower' K K C x

Premises used: minpoly.dvd_map_of_isScalarTower'
-- 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
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'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
⊢ (Polynomial.map (algebraMap K C) (minpoly K (B := C) ((iL : (a : L) → C) x : C))).Splits

Tactic:
exact Polynomial.Splits.of_dvd (sp.of_isScalarTower C)
        (Polynomial.map_ne_zero (minpoly.ne_zero xsep.isIntegral))
        (Polynomial.map_dvd _ (by simpa using minpoly.dvd_map_of_isScalarTower' K K C x))

Premises used: Polynomial.map_dvd, Polynomial.Splits.of_isScalarTower, Polynomial.Splits.of_dvd, Polynomial.map_ne_zero, minpoly.ne_zero, 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
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'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
xC' : C
hx' : IsConjRoot K ((iL : (a : L) → C) x) xC'
hne : (iL : (a : L) → C) x ≠ xC'
rwa :
  ∀ (hx' : xC' ∈ Polynomial.rootSet (minpoly K (B := C) ((iL : (a : L) → C) x : C)) C)
    (hne : (iL : (a : L) → C) x ≠ xC'), xC' ∈ Polynomial.rootSet (minpoly K x) C
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hx' : xC' ∈ Polynomial.rootSet (minpoly K x) C) (hne : (iL : (a : L) → C) x ≠ xC'),
    xC' ∈ Polynomial.rootSet (minpoly K x) C
⊢ xC' ∈ Polynomial.rootSet (minpoly K x) C

Tactic:
rwa [isConjRoot_iff_mem_minpoly_rootSet (xsep.isIntegral.map _),
          minpoly.algHom_eq iL iL.injective x] at hx'

Premises used: isConjRoot_iff_mem_minpoly_rootSet, minpoly.algHom_eq, RingHom.injective, IsIntegral.map, AlgHom.toRingHom, 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
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'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
xC' : C
hx' : IsConjRoot K ((iL : (a : L) → C) x) xC'
hne : (iL : (a : L) → C) x ≠ xC'
⊢ xC' ∈ Polynomial.rootSet (minpoly K x) C

Tactic:
have : xC' ∈ (minpoly K x).rootSet C := by
        rwa [isConjRoot_iff_mem_minpoly_rootSet (xsep.isIntegral.map _),
          minpoly.algHom_eq iL iL.injective x] at hx'
-- 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
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'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this_4 : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
xC' : C
hx' : IsConjRoot K ((iL : (a : L) → C) x) xC'
hne : (iL : (a : L) → C) x ≠ xC'
this : xC' ∈ Polynomial.rootSet (minpoly K x) C
⊢ ∃ x_1 ∈ Polynomial.rootSet (minpoly K x) L, (iL : (a : L) → C) x_1 = xC'

Tactic:
simp only [← sp.image_rootSet iL, Set.mem_image] at this

Premises used: Set.mem_image, Polynomial.Splits.image_rootSet
-- 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
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'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this_4 : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
xC' : C
hx' : IsConjRoot K ((iL : (a : L) → C) x) xC'
hne : (iL : (a : L) → C) x ≠ xC'
this : ∃ x_1 ∈ Polynomial.rootSet (minpoly K x) L, (iL : (a : L) → C) x_1 = xC'
refine_2 :
  ∀ (c : L) (hc : c ∈ Polynomial.rootSet (minpoly K x) L)
    (hx' : IsConjRoot K (A := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C))
    (hne : Ne.{u_1 + 1} (α := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)),
    ‖HSub.hSub (α := C) (β := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) y : C)‖ <
      ‖HSub.hSub (α := C) (β := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)‖
⊢ ‖HSub.hSub (α := C) (β := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) y : C)‖ <
    ‖HSub.hSub (α := C) ((iL : (a : L) → C) x : C) xC'‖

Tactic:
obtain ⟨c, hc, rfl⟩ := this

Premises used: rfl
-- 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
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'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
c : L
hc : c ∈ Polynomial.rootSet (minpoly K x) L
hx' : IsConjRoot K (A := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)
hne : Ne.{u_1 + 1} (α := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)
⊢ IsConjRoot K x c

Tactic:
rw [← isConjRoot_iff_mem_minpoly_rootSet xsep.isIntegral] at hc

Premises used: isConjRoot_iff_mem_minpoly_rootSet, 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
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'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
c : L
hc : c ∈ Polynomial.rootSet (minpoly K x) L
hx' : IsConjRoot K (A := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)
hne : Ne.{u_1 + 1} (α := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)
hc₁ : IsConjRoot K x c
⊢ IsConjRoot K (A := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)

Tactic:
rw [← isConjRoot_iff_mem_minpoly_rootSet xsep.isIntegral] at hc

Premises used: isConjRoot_iff_mem_minpoly_rootSet, 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
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'‖
C : Type u_1 := AlgebraicClosure K
this_1 : NontriviallyNormedField C := spectralNorm.nontriviallyNormedField K C
this_2 : NormedAlgebra K C := spectralNorm.normedAlgebra K C
iL : L →ₐ[K] C := IsAlgClosed.lift
algInst : Algebra L C := iL.toAlgebra
this_3 : NormedAlgebra L C := spectralNorm.normedAlgebra' K L C
this : IsKrasner K C := ⋯
norm_iL : ∀ (x : L), norm.{u_1} (E := C) ((iL : (a : L) → C) x : C) = ‖x‖
c : L
hc : c ∈ Polynomial.rootSet (minpoly K x) L
hx' : IsConjRoot K (A := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)
hne : Ne.{u_1 + 1} (α := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)
hc₁ : IsConjRoot K x c
hx'₁ : IsConjRoot K (A := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)
⊢ Ne.{u_1 + 1} (α := C) ((iL : (a : L) → C) x : C) ((iL : (a : L) → C) c : C)

Tactic:
rw [← isConjRoot_iff_mem_minpoly_rootSet xsep.isIntegral] at hc

Premises used: isConjRoot_iff_mem_minpoly_rootSet, IsSeparable.isIntegral