F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ h = ↑C (leadingCoeff h) * (X - ↑C x)
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
⊢ h = ↑C (leadingCoeff h) * (X - ↑C x)
have h_ne_zero : h ≠ 0 := by
  rintro rfl
  exact not_separable_zero h_sep
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ roots (map i h) = {↑i x}
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ h = ↑C (leadingCoeff h) * (X - ↑C x)
apply Polynomial.eq_X_sub_C_of_splits_of_single_root i h_splits
case x
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ { val := roots (map i h), nodup := ?nodup } = { val := {↑i x}, nodup := ?nodup }

case nodup
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ Multiset.Nodup (roots (map i h))

case nodup
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ Multiset.Nodup {↑i x}
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ roots (map i h) = {↑i x}
apply Finset.mk.inj
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h_sep : Separable 0
h_root : eval x 0 = 0
h_splits : Splits i 0
h_roots : ∀ (y : K), y ∈ roots (map i 0) → y = ↑i x
⊢ False
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
⊢ h ≠ 0
rintro rfl
no goals
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h_sep : Separable 0
h_root : eval x 0 = 0
h_splits : Splits i 0
h_roots : ∀ (y : K), y ∈ roots (map i 0) → y = ↑i x
⊢ False
exact not_separable_zero h_sep
case x
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ { val := roots (map i h), nodup := ?nodup } = {↑i x}
case x
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ { val := roots (map i h), nodup := ?nodup } = { val := {↑i x}, nodup := ?nodup }
change _ = {i x}
case x
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ ↑i x ∈ { val := roots (map i h), nodup := ?nodup } ∧
    ∀ (x_1 : K), x_1 ∈ { val := roots (map i h), nodup := ?nodup } → x_1 = ↑i x

case nodup
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ Multiset.Nodup (roots (map i h))
case x
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ { val := roots (map i h), nodup := ?nodup } = {↑i x}
rw [Finset.eq_singleton_iff_unique_mem]
case x.left
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ ↑i x ∈ { val := roots (map i h), nodup := ?nodup }

case x.right
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ ∀ (x_1 : K), x_1 ∈ { val := roots (map i h), nodup := ?nodup } → x_1 = ↑i x

case nodup
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ Multiset.Nodup (roots (map i h))
case x
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ ↑i x ∈ { val := roots (map i h), nodup := ?nodup } ∧
    ∀ (x_1 : K), x_1 ∈ { val := roots (map i h), nodup := ?nodup } → x_1 = ↑i x

case nodup
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ Multiset.Nodup (roots (map i h))
constructor
case x.left
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ ↑i x ∈ roots (map i h)

case nodup
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ Multiset.Nodup (roots (map i h))
case x.left
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ ↑i x ∈ { val := roots (map i h), nodup := ?nodup }
apply Finset.mem_mk.mpr
case x.left
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ IsRoot (map i h) (↑i x)
case x.left
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ ↑i x ∈ roots (map i h)
rw [mem_roots (show h.map i ≠ 0 from map_ne_zero h_ne_zero)]
case x.left
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ ↑i 0 = 0
case x.left
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ IsRoot (map i h) (↑i x)
rw [IsRoot.def, ← eval₂_eq_eval_map, eval₂_hom, h_root]
no goals
case x.left
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ ↑i 0 = 0
exact RingHom.map_zero i
no goals
case nodup
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ Multiset.Nodup (roots (map i h))
exact nodup_roots (Separable.map h_sep)
no goals
case x.right
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : Separable h
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ (y : K), y ∈ roots (map i h) → y = ↑i x
h_ne_zero : h ≠ 0
⊢ ∀ (x_1 : K), x_1 ∈ { val := roots (map i h), nodup := (_ : Multiset.Nodup (roots (map i h))) } → x_1 = ↑i x
exact h_roots