[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
⊢ dickson k a 2 = X ^ 2 - ↑C a * (3 - ↑k)
[PROOFSTEP]
simp only [dickson, sq]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
n : ℕ
⊢ dickson k a (n + 2) = X * dickson k a (n + 1) - ↑C a * dickson k a n
[PROOFSTEP]
rw [dickson]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
n : ℕ
h : 2 ≤ n
⊢ dickson k a n = X * dickson k a (n - 1) - ↑C a * dickson k a (n - 2)
[PROOFSTEP]
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
n : ℕ
h : 2 ≤ 2 + n
⊢ dickson k a (2 + n) = X * dickson k a (2 + n - 1) - ↑C a * dickson k a (2 + n - 2)
[PROOFSTEP]
rw [add_comm]
[GOAL]
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
n : ℕ
h : 2 ≤ 2 + n
⊢ dickson k a (n + 2) = X * dickson k a (n + 2 - 1) - ↑C a * dickson k a (n + 2 - 2)
[PROOFSTEP]
exact dickson_add_two k a n
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
⊢ map f (dickson k a 0) = dickson k (↑f a) 0
[PROOFSTEP]
simp_rw [dickson_zero, Polynomial.map_sub, Polynomial.map_nat_cast, Polynomial.map_ofNat]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
⊢ map f (dickson k a 1) = dickson k (↑f a) 1
[PROOFSTEP]
simp only [dickson_one, map_X]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
n : ℕ
⊢ map f (dickson k a (n + 2)) = dickson k (↑f a) (n + 2)
[PROOFSTEP]
simp only [dickson_add_two, Polynomial.map_sub, Polynomial.map_mul, map_X, map_C]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
f : R →+* S
n : ℕ
⊢ X * map f (dickson k a (n + 1)) - ↑C (↑f a) * map f (dickson k a n) =
    X * dickson k (↑f a) (n + 1) - ↑C (↑f a) * dickson k (↑f a) n
[PROOFSTEP]
rw [map_dickson f n, map_dickson f (n + 1)]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
⊢ dickson 2 0 0 = X ^ 0
[PROOFSTEP]
simp only [dickson_zero, pow_zero]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
⊢ 3 - ↑2 = 1
[PROOFSTEP]
norm_num
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
⊢ dickson 2 0 1 = X ^ 1
[PROOFSTEP]
simp only [dickson_one, pow_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
n : ℕ
⊢ dickson 2 0 (n + 2) = X ^ (n + 2)
[PROOFSTEP]
simp only [dickson_add_two, C_0, zero_mul, sub_zero]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
n : ℕ
⊢ X * dickson 2 0 (n + 1) = X ^ (n + 2)
[PROOFSTEP]
rw [dickson_two_zero (n + 1), pow_add X (n + 1) 1, mul_comm, pow_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
⊢ eval (x + y) (dickson 1 1 0) = x ^ 0 + y ^ 0
[PROOFSTEP]
suffices eval (x + y) 2 = 2 by convert this <;> norm_num
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
this : eval (x + y) 2 = 2
⊢ eval (x + y) (dickson 1 1 0) = x ^ 0 + y ^ 0
[PROOFSTEP]
convert this
[GOAL]
case h.e'_2.h.e'_4
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
this : eval (x + y) 2 = 2
⊢ dickson 1 1 0 = 2
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_3
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
this : eval (x + y) 2 = 2
⊢ x ^ 0 + y ^ 0 = 2
[PROOFSTEP]
norm_num
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
⊢ eval (x + y) 2 = 2
[PROOFSTEP]
exact eval_nat_cast
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
⊢ eval (x + y) (dickson 1 1 1) = x ^ 1 + y ^ 1
[PROOFSTEP]
simp only [eval_X, dickson_one, pow_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
n : ℕ
⊢ eval (x + y) (dickson 1 1 (n + 2)) = x ^ (n + 2) + y ^ (n + 2)
[PROOFSTEP]
simp only [eval_sub, eval_mul, dickson_one_one_eval_add_inv x y h _, eval_X, dickson_add_two, C_1, eval_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
n : ℕ
⊢ (x + y) * (x ^ (n + 1) + y ^ (n + 1)) - 1 * (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)
[PROOFSTEP]
conv_lhs => simp only [pow_succ, add_mul, mul_add, h, ← mul_assoc, mul_comm y x, one_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
n : ℕ
| (x + y) * (x ^ (n + 1) + y ^ (n + 1)) - 1 * (x ^ n + y ^ n)
[PROOFSTEP]
simp only [pow_succ, add_mul, mul_add, h, ← mul_assoc, mul_comm y x, one_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
n : ℕ
| (x + y) * (x ^ (n + 1) + y ^ (n + 1)) - 1 * (x ^ n + y ^ n)
[PROOFSTEP]
simp only [pow_succ, add_mul, mul_add, h, ← mul_assoc, mul_comm y x, one_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
n : ℕ
| (x + y) * (x ^ (n + 1) + y ^ (n + 1)) - 1 * (x ^ n + y ^ n)
[PROOFSTEP]
simp only [pow_succ, add_mul, mul_add, h, ← mul_assoc, mul_comm y x, one_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a x y : R
h : x * y = 1
n : ℕ
⊢ x * x * x ^ n + x ^ n + (y ^ n + y * y * y ^ n) - (x ^ n + y ^ n) = x ^ (n + 2) + y ^ (n + 2)
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
⊢ 2 * ↑C ⅟2 = 1
[PROOFSTEP]
rw [two_mul, ← C_add, invOf_two_add_invOf_two, C_1]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
⊢ ↑C ⅟2 * 2 = 1
[PROOFSTEP]
rw [mul_comm, two_mul_C_half_eq_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
⊢ dickson 1 1 0 = 2 * comp (Chebyshev.T R 0) (↑C ⅟2 * X)
[PROOFSTEP]
simp only [Chebyshev.T_zero, mul_one, one_comp, dickson_zero]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
⊢ 3 - ↑1 = 2
[PROOFSTEP]
norm_num
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
⊢ dickson 1 1 1 = 2 * comp (Chebyshev.T R 1) (↑C ⅟2 * X)
[PROOFSTEP]
rw [dickson_one, Chebyshev.T_one, X_comp, ← mul_assoc, two_mul_C_half_eq_one, one_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
n : ℕ
⊢ dickson 1 1 (n + 2) = 2 * comp (Chebyshev.T R (n + 2)) (↑C ⅟2 * X)
[PROOFSTEP]
rw [dickson_add_two, C_1, Chebyshev.T_add_two, dickson_one_one_eq_chebyshev_T (n + 1), dickson_one_one_eq_chebyshev_T n,
  sub_comp, mul_comp, mul_comp, X_comp, ofNat_comp]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
n : ℕ
⊢ X * (2 * comp (Chebyshev.T R (n + 1)) (↑C ⅟2 * X)) - 1 * (2 * comp (Chebyshev.T R n) (↑C ⅟2 * X)) =
    2 * (↑2 * (↑C ⅟2 * X) * comp (Chebyshev.T R (n + 1)) (↑C ⅟2 * X) - comp (Chebyshev.T R n) (↑C ⅟2 * X))
[PROOFSTEP]
simp_rw [← mul_assoc, Nat.cast_ofNat, two_mul_C_half_eq_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
n : ℕ
⊢ X * 2 * comp (Chebyshev.T R (n + 1)) (↑C ⅟2 * X) - 1 * 2 * comp (Chebyshev.T R n) (↑C ⅟2 * X) =
    2 * (1 * X * comp (Chebyshev.T R (n + 1)) (↑C ⅟2 * X) - comp (Chebyshev.T R n) (↑C ⅟2 * X))
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
n : ℕ
⊢ Chebyshev.T R n = ↑C ⅟2 * comp (dickson 1 1 n) (2 * X)
[PROOFSTEP]
rw [dickson_one_one_eq_chebyshev_T, mul_comp, ofNat_comp, comp_assoc, mul_comp, C_comp, X_comp]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
inst✝ : Invertible 2
n : ℕ
⊢ Chebyshev.T R n = ↑C ⅟2 * (↑2 * comp (Chebyshev.T R n) (↑C ⅟2 * (2 * X)))
[PROOFSTEP]
simp_rw [← mul_assoc, Nat.cast_ofNat, C_half_mul_two_eq_one, one_mul, comp_X]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
⊢ dickson 1 1 (m * n) = comp (dickson 1 1 m) (dickson 1 1 n)
[PROOFSTEP]
have h : (1 : R) = Int.castRingHom R 1
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
⊢ 1 = ↑(Int.castRingHom R) 1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ dickson 1 1 (m * n) = comp (dickson 1 1 m) (dickson 1 1 n)
[PROOFSTEP]
simp only [eq_intCast, Int.cast_one]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ dickson 1 1 (m * n) = comp (dickson 1 1 m) (dickson 1 1 n)
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ dickson 1 (↑(Int.castRingHom R) 1) (m * n) =
    comp (dickson 1 (↑(Int.castRingHom R) 1) m) (dickson 1 (↑(Int.castRingHom R) 1) n)
[PROOFSTEP]
simp only [← map_dickson (Int.castRingHom R), ← map_comp]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ map (Int.castRingHom R) (dickson 1 1 (m * n)) = map (Int.castRingHom R) (comp (dickson 1 1 m) (dickson 1 1 n))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ dickson 1 1 (m * n) = comp (dickson 1 1 m) (dickson 1 1 n)
[PROOFSTEP]
apply map_injective (Int.castRingHom ℚ) Int.cast_injective
[GOAL]
case e_a.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ map (Int.castRingHom ℚ) (dickson 1 1 (m * n)) = map (Int.castRingHom ℚ) (comp (dickson 1 1 m) (dickson 1 1 n))
[PROOFSTEP]
simp only [map_dickson, map_comp, eq_intCast, Int.cast_one, dickson_one_one_eq_chebyshev_T, Chebyshev.T_mul, two_mul, ←
  add_comp]
[GOAL]
case e_a.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ comp (comp (Chebyshev.T ℚ m + Chebyshev.T ℚ m) (Chebyshev.T ℚ n)) (↑C ⅟2 * X) =
    comp (comp (Chebyshev.T ℚ m + Chebyshev.T ℚ m) (↑C ⅟2 * X)) (comp (Chebyshev.T ℚ n + Chebyshev.T ℚ n) (↑C ⅟2 * X))
[PROOFSTEP]
simp only [← two_mul, ← comp_assoc]
[GOAL]
case e_a.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ comp (comp (2 * Chebyshev.T ℚ m) (Chebyshev.T ℚ n)) (↑C ⅟2 * X) =
    comp (comp (comp (2 * Chebyshev.T ℚ m) (↑C ⅟2 * X)) (2 * Chebyshev.T ℚ n)) (↑C ⅟2 * X)
[PROOFSTEP]
apply eval₂_congr rfl rfl
[GOAL]
case e_a.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ comp (2 * Chebyshev.T ℚ m) (Chebyshev.T ℚ n) = comp (comp (2 * Chebyshev.T ℚ m) (↑C ⅟2 * X)) (2 * Chebyshev.T ℚ n)
[PROOFSTEP]
rw [comp_assoc]
[GOAL]
case e_a.a
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ comp (2 * Chebyshev.T ℚ m) (Chebyshev.T ℚ n) = comp (2 * Chebyshev.T ℚ m) (comp (↑C ⅟2 * X) (2 * Chebyshev.T ℚ n))
[PROOFSTEP]
apply eval₂_congr rfl _ rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
h : 1 = ↑(Int.castRingHom R) 1
⊢ Chebyshev.T ℚ n = comp (↑C ⅟2 * X) (2 * Chebyshev.T ℚ n)
[PROOFSTEP]
rw [mul_comp, C_comp, X_comp, ← mul_assoc, C_half_mul_two_eq_one, one_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
k : ℕ
a : R
m n : ℕ
⊢ comp (dickson 1 1 m) (dickson 1 1 n) = comp (dickson 1 1 n) (dickson 1 1 m)
[PROOFSTEP]
rw [← dickson_one_one_mul, mul_comm, dickson_one_one_mul]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ dickson 1 1 p = X ^ p
[PROOFSTEP]
obtain ⟨K, _, _, H⟩ : ∃ (K : Type) (_ : Field K), ∃ _ : CharP K p, Infinite K :=
  by
  let K := FractionRing (Polynomial (ZMod p))
  let f : ZMod p →+* K := (algebraMap _ (FractionRing _)).comp C
  have : CharP K p := by
    rw [← f.charP_iff_charP]
    infer_instance
  haveI : Infinite K :=
    Infinite.of_injective (algebraMap (Polynomial (ZMod p)) (FractionRing (Polynomial (ZMod p))))
      (IsFractionRing.injective _ _)
  refine' ⟨K, _, _, _⟩ <;> infer_instance
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∃ K x x, Infinite K
[PROOFSTEP]
let K := FractionRing (Polynomial (ZMod p))
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
⊢ ∃ K x x, Infinite K
[PROOFSTEP]
let f : ZMod p →+* K := (algebraMap _ (FractionRing _)).comp C
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
⊢ ∃ K x x, Infinite K
[PROOFSTEP]
have : CharP K p := by
  rw [← f.charP_iff_charP]
  infer_instance
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
⊢ CharP K p
[PROOFSTEP]
rw [← f.charP_iff_charP]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
⊢ CharP (ZMod p) p
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
this : CharP K p
⊢ ∃ K x x, Infinite K
[PROOFSTEP]
haveI : Infinite K :=
  Infinite.of_injective (algebraMap (Polynomial (ZMod p)) (FractionRing (Polynomial (ZMod p))))
    (IsFractionRing.injective _ _)
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
this✝ : CharP K p
this : Infinite K
⊢ ∃ K x x, Infinite K
[PROOFSTEP]
refine' ⟨K, _, _, _⟩
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
this✝ : CharP K p
this : Infinite K
⊢ Field K
[PROOFSTEP]
infer_instance
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
this✝ : CharP K p
this : Infinite K
⊢ CharP K p
[PROOFSTEP]
infer_instance
[GOAL]
case refine'_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type := FractionRing (ZMod p)[X]
f : ZMod p →+* K := RingHom.comp (algebraMap (ZMod p)[X] (FractionRing (ZMod p)[X])) C
this✝ : CharP K p
this : Infinite K
⊢ Infinite K
[PROOFSTEP]
infer_instance
[GOAL]
case intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ dickson 1 1 p = X ^ p
[PROOFSTEP]
apply map_injective (ZMod.castHom (dvd_refl p) K) (RingHom.injective _)
[GOAL]
case intro.intro.intro.a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ map (ZMod.castHom (_ : p ∣ p) K) (dickson 1 1 p) = map (ZMod.castHom (_ : p ∣ p) K) (X ^ p)
[PROOFSTEP]
rw [map_dickson, Polynomial.map_pow, map_X]
[GOAL]
case intro.intro.intro.a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ dickson 1 (↑(ZMod.castHom (_ : p ∣ p) K) 1) p = X ^ p
[PROOFSTEP]
apply eq_of_infinite_eval_eq
[GOAL]
case intro.intro.intro.a.h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ Set.Infinite {x | eval x (dickson 1 (↑(ZMod.castHom (_ : p ∣ p) K) 1) p) = eval x (X ^ p)}
[PROOFSTEP]
apply @Set.Infinite.mono _ {x : K | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
[GOAL]
case intro.intro.intro.a.h.h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0} ⊆ {x | eval x (dickson 1 (↑(ZMod.castHom (_ : p ∣ p) K) 1) p) = eval x (X ^ p)}
[PROOFSTEP]
rintro _ ⟨x, rfl, hx⟩
[GOAL]
case intro.intro.intro.a.h.h.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
x : K
hx : x ≠ 0
⊢ x + x⁻¹ ∈ {x | eval x (dickson 1 (↑(ZMod.castHom (_ : p ∣ p) K) 1) p) = eval x (X ^ p)}
[PROOFSTEP]
simp only [eval_X, eval_pow, Set.mem_setOf_eq, @add_pow_char K _ p,
  dickson_one_one_eval_add_inv _ _ (mul_inv_cancel hx), inv_pow, ZMod.castHom_apply, ZMod.cast_one']
  -- Now we need to show that the set of such `x` is infinite.
    -- If the set is finite, then we will show that `K` is also finite.
[GOAL]
case intro.intro.intro.a.h.a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
⊢ Set.Infinite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
[PROOFSTEP]
intro h
[GOAL]
case intro.intro.intro.a.h.a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Infinite K
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ False
[PROOFSTEP]
rw [← Set.infinite_univ_iff] at H
[GOAL]
case intro.intro.intro.a.h.a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ False
[PROOFSTEP]
apply H
[GOAL]
case intro.intro.intro.a.h.a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ Set.Finite Set.univ
[PROOFSTEP]
suffices (Set.univ : Set K) = {x : K | ∃ y : K, x = y + y⁻¹ ∧ y ≠ 0} >>= fun x => {y | x = y + y⁻¹ ∨ y = 0}
  by
  rw [this]
  clear this
  refine'
    h.biUnion fun x _ =>
      _
        -- The following quadratic polynomial has as solutions the `y` for which `x = y + y⁻¹`.
  let φ : K[X] := X ^ 2 - C x * X + 1
  have hφ : φ ≠ 0 := by
    intro H
    have : φ.eval 0 = 0 := by rw [H, eval_zero]
    simpa [eval_X, eval_one, eval_pow, eval_sub, sub_zero, eval_add, eval_mul, mul_zero, sq, zero_add, one_ne_zero]
  classical
  convert (φ.roots ∪ {0}).toFinset.finite_toSet using 1
  ext1 y
  simp only [Multiset.mem_toFinset, Set.mem_setOf_eq, Finset.mem_coe, Multiset.mem_union, mem_roots hφ, IsRoot,
    eval_add, eval_sub, eval_pow, eval_mul, eval_X, eval_C, eval_one, Multiset.mem_singleton]
  by_cases hy : y = 0
  · simp only [hy, eq_self_iff_true, or_true_iff]
  apply or_congr _ Iff.rfl
  rw [← mul_left_inj' hy, eq_comm, ← sub_eq_zero, add_mul, inv_mul_cancel hy]
  apply eq_iff_eq_cancel_right.mpr
  ring
    -- Finally, we prove the claim that our finite union of finite sets covers all of `K`.
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
this :
  Set.univ = do
    let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
    {y | x = y + y⁻¹ ∨ y = 0}
⊢ Set.Finite Set.univ
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
this :
  Set.univ = do
    let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
    {y | x = y + y⁻¹ ∨ y = 0}
⊢ Set.Finite do
    let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
    {y | x = y + y⁻¹ ∨ y = 0}
[PROOFSTEP]
clear this
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ Set.Finite do
    let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
    {y | x = y + y⁻¹ ∨ y = 0}
[PROOFSTEP]
refine'
  h.biUnion fun x _ =>
    _
      -- The following quadratic polynomial has as solutions the `y` for which `x = y + y⁻¹`.
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ Set.Finite ((fun x => {y | x = y + y⁻¹ ∨ y = 0}) x)
[PROOFSTEP]
let φ : K[X] := X ^ 2 - C x * X + 1
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
⊢ Set.Finite ((fun x => {y | x = y + y⁻¹ ∨ y = 0}) x)
[PROOFSTEP]
have hφ : φ ≠ 0 := by
  intro H
  have : φ.eval 0 = 0 := by rw [H, eval_zero]
  simpa [eval_X, eval_one, eval_pow, eval_sub, sub_zero, eval_add, eval_mul, mul_zero, sq, zero_add, one_ne_zero]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
⊢ φ ≠ 0
[PROOFSTEP]
intro H
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H✝ : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
H : φ = 0
⊢ False
[PROOFSTEP]
have : φ.eval 0 = 0 := by rw [H, eval_zero]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H✝ : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
H : φ = 0
⊢ eval 0 φ = 0
[PROOFSTEP]
rw [H, eval_zero]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H✝ : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
H : φ = 0
this : eval 0 φ = 0
⊢ False
[PROOFSTEP]
simpa [eval_X, eval_one, eval_pow, eval_sub, sub_zero, eval_add, eval_mul, mul_zero, sq, zero_add, one_ne_zero]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
hφ : φ ≠ 0
⊢ Set.Finite ((fun x => {y | x = y + y⁻¹ ∨ y = 0}) x)
[PROOFSTEP]
classical
convert (φ.roots ∪ {0}).toFinset.finite_toSet using 1
ext1 y
simp only [Multiset.mem_toFinset, Set.mem_setOf_eq, Finset.mem_coe, Multiset.mem_union, mem_roots hφ, IsRoot, eval_add,
  eval_sub, eval_pow, eval_mul, eval_X, eval_C, eval_one, Multiset.mem_singleton]
by_cases hy : y = 0
· simp only [hy, eq_self_iff_true, or_true_iff]
apply or_congr _ Iff.rfl
rw [← mul_left_inj' hy, eq_comm, ← sub_eq_zero, add_mul, inv_mul_cancel hy]
apply eq_iff_eq_cancel_right.mpr
ring
  -- Finally, we prove the claim that our finite union of finite sets covers all of `K`.
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
hφ : φ ≠ 0
⊢ Set.Finite ((fun x => {y | x = y + y⁻¹ ∨ y = 0}) x)
[PROOFSTEP]
convert (φ.roots ∪ {0}).toFinset.finite_toSet using 1
[GOAL]
case h.e'_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
hφ : φ ≠ 0
⊢ (fun x => {y | x = y + y⁻¹ ∨ y = 0}) x = ↑(Multiset.toFinset (roots φ ∪ {0}))
[PROOFSTEP]
ext1 y
[GOAL]
case h.e'_2.h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
hφ : φ ≠ 0
y : K
⊢ y ∈ (fun x => {y | x = y + y⁻¹ ∨ y = 0}) x ↔ y ∈ ↑(Multiset.toFinset (roots φ ∪ {0}))
[PROOFSTEP]
simp only [Multiset.mem_toFinset, Set.mem_setOf_eq, Finset.mem_coe, Multiset.mem_union, mem_roots hφ, IsRoot, eval_add,
  eval_sub, eval_pow, eval_mul, eval_X, eval_C, eval_one, Multiset.mem_singleton]
[GOAL]
case h.e'_2.h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
hφ : φ ≠ 0
y : K
⊢ x = y + y⁻¹ ∨ y = 0 ↔ y ^ 2 - x * y + 1 = 0 ∨ y = 0
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
hφ : φ ≠ 0
y : K
hy : y = 0
⊢ x = y + y⁻¹ ∨ y = 0 ↔ y ^ 2 - x * y + 1 = 0 ∨ y = 0
[PROOFSTEP]
simp only [hy, eq_self_iff_true, or_true_iff]
[GOAL]
case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
⊢ x = y + y⁻¹ ∨ y = 0 ↔ y ^ 2 - x * y + 1 = 0 ∨ y = 0
[PROOFSTEP]
apply or_congr _ Iff.rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
⊢ x = y + y⁻¹ ↔ y ^ 2 - x * y + 1 = 0
[PROOFSTEP]
rw [← mul_left_inj' hy, eq_comm, ← sub_eq_zero, add_mul, inv_mul_cancel hy]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
⊢ y * y + 1 - x * y = 0 ↔ y ^ 2 - x * y + 1 = 0
[PROOFSTEP]
apply eq_iff_eq_cancel_right.mpr
[GOAL]
case a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - ↑C x * X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
⊢ y * y + 1 - x * y = y ^ 2 - x * y + 1
[PROOFSTEP]
ring
  -- Finally, we prove the claim that our finite union of finite sets covers all of `K`.
[GOAL]
case intro.intro.intro.a.h.a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ Set.univ = do
    let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
    {y | x = y + y⁻¹ ∨ y = 0}
[PROOFSTEP]
apply (Set.eq_univ_of_forall _).symm
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
⊢ ∀ (x : K),
    x ∈ do
      let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
      {y | x = y + y⁻¹ ∨ y = 0}
[PROOFSTEP]
intro x
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
⊢ x ∈ do
    let x ← {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
    {y | x = y + y⁻¹ ∨ y = 0}
[PROOFSTEP]
simp only [exists_prop, Set.mem_iUnion, Set.bind_def, Ne.def, Set.mem_setOf_eq]
[GOAL]
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
⊢ ∃ i, (∃ y, i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : x = 0
⊢ ∃ i, (∃ y, i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
[PROOFSTEP]
simp only [hx, and_true_iff, eq_self_iff_true, inv_zero, or_true_iff]
[GOAL]
case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : x = 0
⊢ ∃ i y, i = y + y⁻¹ ∧ ¬y = 0
[PROOFSTEP]
exact ⟨_, 1, rfl, one_ne_zero⟩
[GOAL]
case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : ¬x = 0
⊢ ∃ i, (∃ y, i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)
[PROOFSTEP]
simp only [hx, or_false_iff, exists_eq_right]
[GOAL]
case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
k : ℕ
a : R
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.Infinite Set.univ
h : Set.Finite {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
x : K
hx : ¬x = 0
⊢ ∃ y, x + x⁻¹ = y + y⁻¹ ∧ ¬y = 0
[PROOFSTEP]
exact ⟨_, rfl, hx⟩
[GOAL]
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
k : ℕ
a : R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
⊢ dickson 1 1 p = X ^ p
[PROOFSTEP]
have h : (1 : R) = ZMod.castHom (dvd_refl p) R 1
[GOAL]
case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
k : ℕ
a : R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
⊢ 1 = ↑(ZMod.castHom (_ : p ∣ p) R) 1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
k : ℕ
a : R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
h : 1 = ↑(ZMod.castHom (_ : p ∣ p) R) 1
⊢ dickson 1 1 p = X ^ p
[PROOFSTEP]
simp only [ZMod.castHom_apply, ZMod.cast_one']
[GOAL]
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
k : ℕ
a : R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
h : 1 = ↑(ZMod.castHom (_ : p ∣ p) R) 1
⊢ dickson 1 1 p = X ^ p
[PROOFSTEP]
rw [h, ← map_dickson (ZMod.castHom (dvd_refl p) R), dickson_one_one_zmod_p, Polynomial.map_pow, map_X]


[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (↑C r * X ^ n)
[PROOFSTEP]
refine' Commute.isNilpotent_mul_left (commute_X_pow _ _).symm _
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (↑C r)
[PROOFSTEP]
obtain ⟨m, hm⟩ := hnil
[GOAL]
case intro
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
n m : ℕ
hm : r ^ m = 0
⊢ IsNilpotent (↑C r)
[PROOFSTEP]
refine' ⟨m, _⟩
[GOAL]
case intro
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
n m : ℕ
hm : r ^ m = 0
⊢ ↑C r ^ m = 0
[PROOFSTEP]
rw [← C_pow, hm, C_0]
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (X ^ n * ↑C r)
[PROOFSTEP]
rw [commute_X_pow]
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (↑C r * X ^ n)
[PROOFSTEP]
exact isNilpotent_C_mul_pow_X_of_isNilpotent n hnil
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
n k : ℕ
⊢ ↑(monomial n) r ^ k = 0 ↔ r ^ k = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
k : ℕ
⊢ ↑C r ^ k = 0 ↔ r ^ k = 0
[PROOFSTEP]
simpa only [← C_pow] using C_eq_zero
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent (X * P) ↔ IsNilpotent P
[PROOFSTEP]
refine' ⟨fun h ↦ _, _⟩
[GOAL]
case refine'_1
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
h : IsNilpotent (X * P)
⊢ IsNilpotent P
[PROOFSTEP]
rwa [Commute.isNilpotent_mul_right_iff (commute_X P) (by simp)] at h
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
h : IsNilpotent (X * P)
⊢ X ∈ nonZeroDivisorsRight R[X]
[PROOFSTEP]
simp
[GOAL]
case refine'_2
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent P → IsNilpotent (X * P)
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case refine'_2.intro
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
k : ℕ
hk : P ^ k = 0
⊢ IsNilpotent (X * P)
[PROOFSTEP]
exact ⟨k, by simp [(commute_X P).mul_pow, hk]⟩
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
k : ℕ
hk : P ^ k = 0
⊢ (X * P) ^ k = 0
[PROOFSTEP]
simp [(commute_X P).mul_pow, hk]
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent (P * X) ↔ IsNilpotent P
[PROOFSTEP]
rw [← commute_X P]
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent (X * P) ↔ IsNilpotent P
[PROOFSTEP]
exact isNilpotent_X_mul_iff
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ IsNilpotent P ↔ ∀ (i : ℕ), IsNilpotent (coeff P i)
[PROOFSTEP]
refine' ⟨P.recOnHorner (by simp) (fun p r hp₀ _ hp hpr i ↦ _) (fun p _ hnp hpX i ↦ _), fun h ↦ _⟩
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ IsNilpotent 0 → ∀ (i : ℕ), IsNilpotent (coeff 0 i)
[PROOFSTEP]
simp
[GOAL]
case refine'_1
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P i)
⊢ IsNilpotent P
[PROOFSTEP]
rw [← sum_monomial_eq P]
[GOAL]
case refine'_1
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P i)
⊢ IsNilpotent (sum P fun n a => ↑(monomial n) a)
[PROOFSTEP]
exact isNilpotent_sum (fun i _ ↦ by simpa only [isNilpotent_monomial_iff] using h i)
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P i)
i : ℕ
x✝ : i ∈ support P
⊢ IsNilpotent ((fun n a => ↑(monomial n) a) i (coeff P i))
[PROOFSTEP]
simpa only [isNilpotent_monomial_iff] using h i
[GOAL]
case refine'_2
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpr : IsNilpotent (p + ↑C r)
i : ℕ
⊢ IsNilpotent (coeff (p + ↑C r) i)
[PROOFSTEP]
have hr : IsNilpotent (C r) := by
  obtain ⟨k, hk⟩ := hpr
  replace hp : eval 0 p = 0 := by rwa [coeff_zero_eq_aeval_zero] at hp₀
  refine' isNilpotent_C_iff.mpr ⟨k, _⟩
  simpa [coeff_zero_eq_aeval_zero, hp] using congr_arg (fun q ↦ coeff q 0) hk
[GOAL]
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpr : IsNilpotent (p + ↑C r)
i : ℕ
⊢ IsNilpotent (↑C r)
[PROOFSTEP]
obtain ⟨k, hk⟩ := hpr
[GOAL]
case intro
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
i k : ℕ
hk : (p + ↑C r) ^ k = 0
⊢ IsNilpotent (↑C r)
[PROOFSTEP]
replace hp : eval 0 p = 0 := by rwa [coeff_zero_eq_aeval_zero] at hp₀
[GOAL]
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
i k : ℕ
hk : (p + ↑C r) ^ k = 0
⊢ eval 0 p = 0
[PROOFSTEP]
rwa [coeff_zero_eq_aeval_zero] at hp₀
[GOAL]
case intro
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
i k : ℕ
hk : (p + ↑C r) ^ k = 0
hp : eval 0 p = 0
⊢ IsNilpotent (↑C r)
[PROOFSTEP]
refine' isNilpotent_C_iff.mpr ⟨k, _⟩
[GOAL]
case intro
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
i k : ℕ
hk : (p + ↑C r) ^ k = 0
hp : eval 0 p = 0
⊢ r ^ k = 0
[PROOFSTEP]
simpa [coeff_zero_eq_aeval_zero, hp] using congr_arg (fun q ↦ coeff q 0) hk
[GOAL]
case refine'_2
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpr : IsNilpotent (p + ↑C r)
i : ℕ
hr : IsNilpotent (↑C r)
⊢ IsNilpotent (coeff (p + ↑C r) i)
[PROOFSTEP]
cases' i with i
[GOAL]
case refine'_2.zero
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpr : IsNilpotent (p + ↑C r)
hr : IsNilpotent (↑C r)
⊢ IsNilpotent (coeff (p + ↑C r) Nat.zero)
case refine'_2.succ
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpr : IsNilpotent (p + ↑C r)
hr : IsNilpotent (↑C r)
i : ℕ
⊢ IsNilpotent (coeff (p + ↑C r) (Nat.succ i))
[PROOFSTEP]
simpa [hp₀] using hr
[GOAL]
case refine'_2.succ
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpr : IsNilpotent (p + ↑C r)
hr : IsNilpotent (↑C r)
i : ℕ
⊢ IsNilpotent (coeff (p + ↑C r) (Nat.succ i))
[PROOFSTEP]
simp only [coeff_add, coeff_C_succ, add_zero]
[GOAL]
case refine'_2.succ
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpr : IsNilpotent (p + ↑C r)
hr : IsNilpotent (↑C r)
i : ℕ
⊢ IsNilpotent (coeff p (Nat.succ i))
[PROOFSTEP]
apply hp
[GOAL]
case refine'_2.succ.a
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpr : IsNilpotent (p + ↑C r)
hr : IsNilpotent (↑C r)
i : ℕ
⊢ IsNilpotent p
[PROOFSTEP]
simpa using Commute.isNilpotent_sub (Commute.all _ _) hpr hr
[GOAL]
case refine'_3
R : Type u_1
r : R
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpX : IsNilpotent (p * X)
i : ℕ
⊢ IsNilpotent (coeff (p * X) i)
[PROOFSTEP]
cases' i with i
[GOAL]
case refine'_3.zero
R : Type u_1
r : R
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpX : IsNilpotent (p * X)
⊢ IsNilpotent (coeff (p * X) Nat.zero)
case refine'_3.succ
R : Type u_1
r : R
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpX : IsNilpotent (p * X)
i : ℕ
⊢ IsNilpotent (coeff (p * X) (Nat.succ i))
[PROOFSTEP]
simp
[GOAL]
case refine'_3.succ
R : Type u_1
r : R
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpX : IsNilpotent (p * X)
i : ℕ
⊢ IsNilpotent (coeff (p * X) (Nat.succ i))
[PROOFSTEP]
simpa using hnp (isNilpotent_mul_X_iff.mp hpX) i
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ IsNilpotent (reverse P) ↔ IsNilpotent P
[PROOFSTEP]
simp only [Polynomial.isNilpotent_iff, coeff_reverse]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ (∀ (i : ℕ), IsNilpotent (coeff P (↑(revAt (natDegree P)) i))) ↔ ∀ (i : ℕ), IsNilpotent (coeff P i)
[PROOFSTEP]
refine' ⟨fun h i ↦ _, fun h i ↦ _⟩
[GOAL]
case refine'_1
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P (↑(revAt (natDegree P)) i))
i : ℕ
⊢ IsNilpotent (coeff P i)
[PROOFSTEP]
cases' le_or_lt i P.natDegree with hi hi
[GOAL]
case refine'_2
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P i)
i : ℕ
⊢ IsNilpotent (coeff P (↑(revAt (natDegree P)) i))
[PROOFSTEP]
cases' le_or_lt i P.natDegree with hi hi
[GOAL]
case refine'_1.inl
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P (↑(revAt (natDegree P)) i))
i : ℕ
hi : i ≤ natDegree P
⊢ IsNilpotent (coeff P i)
[PROOFSTEP]
simpa [tsub_tsub_cancel_of_le hi] using h (P.natDegree - i)
[GOAL]
case refine'_1.inr
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P (↑(revAt (natDegree P)) i))
i : ℕ
hi : natDegree P < i
⊢ IsNilpotent (coeff P i)
[PROOFSTEP]
simp [coeff_eq_zero_of_natDegree_lt hi]
[GOAL]
case refine'_2.inl
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P i)
i : ℕ
hi : i ≤ natDegree P
⊢ IsNilpotent (coeff P (↑(revAt (natDegree P)) i))
[PROOFSTEP]
simpa only [hi, revAt_le] using h (P.natDegree - i)
[GOAL]
case refine'_2.inr
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P i)
i : ℕ
hi : natDegree P < i
⊢ IsNilpotent (coeff P (↑(revAt (natDegree P)) i))
[PROOFSTEP]
simpa only [revAt_eq_self_of_lt hi] using h i
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
⊢ IsUnit P
[PROOFSTEP]
induction' h : P.natDegree using Nat.strong_induction_on with k hind generalizing P
[GOAL]
case h
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
⊢ IsUnit P
[PROOFSTEP]
by_cases hdeg : P.natDegree = 0
[GOAL]
case pos
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : natDegree P = 0
⊢ IsUnit P
case neg
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
⊢ IsUnit P
[PROOFSTEP]
{ rw [eq_C_of_natDegree_eq_zero hdeg]
  exact hunit.map C
}
[GOAL]
case pos
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : natDegree P = 0
⊢ IsUnit P
[PROOFSTEP]
rw [eq_C_of_natDegree_eq_zero hdeg]
[GOAL]
case pos
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : natDegree P = 0
⊢ IsUnit (↑C (coeff P 0))
[PROOFSTEP]
exact hunit.map C
[GOAL]
case neg
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
⊢ IsUnit P
[PROOFSTEP]
set P₁ := P.eraseLead with hP₁
[GOAL]
case neg
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
⊢ IsUnit P
[PROOFSTEP]
suffices IsUnit P₁ by
  rw [← eraseLead_add_monomial_natDegree_leadingCoeff P, ← C_mul_X_pow_eq_monomial]
  obtain ⟨Q, hQ⟩ := this
  rw [← hP₁, ← hQ]
  refine'
    Commute.IsNilpotent.add_isUnit (isNilpotent_C_mul_pow_X_of_isNilpotent _ (hnil _ hdeg))
      ((Commute.all _ _).mul_left (Commute.all _ _))
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
this : IsUnit P₁
⊢ IsUnit P
[PROOFSTEP]
rw [← eraseLead_add_monomial_natDegree_leadingCoeff P, ← C_mul_X_pow_eq_monomial]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
this : IsUnit P₁
⊢ IsUnit (eraseLead P + ↑C (leadingCoeff P) * X ^ natDegree P)
[PROOFSTEP]
obtain ⟨Q, hQ⟩ := this
[GOAL]
case intro
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
Q : R[X]ˣ
hQ : ↑Q = P₁
⊢ IsUnit (eraseLead P + ↑C (leadingCoeff P) * X ^ natDegree P)
[PROOFSTEP]
rw [← hP₁, ← hQ]
[GOAL]
case intro
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
Q : R[X]ˣ
hQ : ↑Q = P₁
⊢ IsUnit (↑Q + ↑C (leadingCoeff P) * X ^ natDegree P)
[PROOFSTEP]
refine'
  Commute.IsNilpotent.add_isUnit (isNilpotent_C_mul_pow_X_of_isNilpotent _ (hnil _ hdeg))
    ((Commute.all _ _).mul_left (Commute.all _ _))
[GOAL]
case neg
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
⊢ IsUnit P₁
[PROOFSTEP]
have hdeg₂ := lt_of_le_of_lt P.eraseLead_natDegree_le (Nat.sub_lt (Nat.pos_of_ne_zero hdeg) zero_lt_one)
[GOAL]
case neg
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
hdeg₂ : natDegree (eraseLead P) < natDegree P
⊢ IsUnit P₁
[PROOFSTEP]
refine' hind P₁.natDegree _ _ (fun i hi => _) rfl
[GOAL]
case neg.refine'_1
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
hdeg₂ : natDegree (eraseLead P) < natDegree P
⊢ natDegree P₁ < k
[PROOFSTEP]
simp_rw [← h, hdeg₂]
[GOAL]
case neg.refine'_2
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
hdeg₂ : natDegree (eraseLead P) < natDegree P
⊢ IsUnit (coeff P₁ 0)
[PROOFSTEP]
simp_rw [eraseLead_coeff_of_ne _ (Ne.symm hdeg), hunit]
[GOAL]
case neg.refine'_3
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
hdeg₂ : natDegree (eraseLead P) < natDegree P
i : ℕ
hi : i ≠ 0
⊢ IsNilpotent (coeff P₁ i)
[PROOFSTEP]
by_cases H : i ≤ P₁.natDegree
[GOAL]
case pos
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
hdeg₂ : natDegree (eraseLead P) < natDegree P
i : ℕ
hi : i ≠ 0
H : i ≤ natDegree P₁
⊢ IsNilpotent (coeff P₁ i)
case neg
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
hdeg₂ : natDegree (eraseLead P) < natDegree P
i : ℕ
hi : i ≠ 0
H : ¬i ≤ natDegree P₁
⊢ IsNilpotent (coeff P₁ i)
[PROOFSTEP]
simp_rw [eraseLead_coeff_of_ne _ (ne_of_lt (lt_of_le_of_lt H hdeg₂)), hnil i hi]
[GOAL]
case neg
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
hdeg₂ : natDegree (eraseLead P) < natDegree P
i : ℕ
hi : i ≠ 0
H : ¬i ≤ natDegree P₁
⊢ IsNilpotent (coeff P₁ i)
[PROOFSTEP]
simp_rw [coeff_eq_zero_of_natDegree_lt (lt_of_not_ge H), IsNilpotent.zero]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
⊢ IsUnit (coeff P 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
[PROOFSTEP]
obtain ⟨Q, hQ⟩ := IsUnit.exists_right_inv hunit
[GOAL]
case intro
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
⊢ IsUnit (coeff P 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
[PROOFSTEP]
constructor
[GOAL]
case intro.left
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
⊢ IsUnit (coeff P 0)
[PROOFSTEP]
refine' isUnit_of_mul_eq_one _ (Q.coeff 0) _
[GOAL]
case intro.left
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
⊢ coeff P 0 * coeff Q 0 = 1
[PROOFSTEP]
have h := (mul_coeff_zero P Q).symm
[GOAL]
case intro.left
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
h : coeff P 0 * coeff Q 0 = coeff (P * Q) 0
⊢ coeff P 0 * coeff Q 0 = 1
[PROOFSTEP]
rwa [hQ, coeff_one_zero] at h
[GOAL]
case intro.right
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
⊢ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
[PROOFSTEP]
intros n hn
[GOAL]
case intro.right
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
⊢ IsNilpotent (coeff P n)
[PROOFSTEP]
rw [nilpotent_iff_mem_prime]
[GOAL]
case intro.right
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
⊢ ∀ (J : Ideal R), Ideal.IsPrime J → coeff P n ∈ J
[PROOFSTEP]
intros I hI
[GOAL]
case intro.right
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
⊢ coeff P n ∈ I
[PROOFSTEP]
let f := mapRingHom (Ideal.Quotient.mk I)
[GOAL]
case intro.right
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
⊢ coeff P n ∈ I
[PROOFSTEP]
have hPQ : degree (f P) = 0 ∧ degree (f Q) = 0 := by
  rw [← Nat.WithBot.add_eq_zero_iff, ← degree_mul, ← _root_.map_mul, hQ, map_one, degree_one]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
⊢ degree (↑f P) = 0 ∧ degree (↑f Q) = 0
[PROOFSTEP]
rw [← Nat.WithBot.add_eq_zero_iff, ← degree_mul, ← _root_.map_mul, hQ, map_one, degree_one]
[GOAL]
case intro.right
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : degree (↑f P) = 0 ∧ degree (↑f Q) = 0
⊢ coeff P n ∈ I
[PROOFSTEP]
have hcoeff : (f P).coeff n = 0 := by
  refine' coeff_eq_zero_of_degree_lt _
  rw [hPQ.1]
  exact (@WithBot.coe_pos _ _ _ n).2 (Ne.bot_lt hn)
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : degree (↑f P) = 0 ∧ degree (↑f Q) = 0
⊢ coeff (↑f P) n = 0
[PROOFSTEP]
refine' coeff_eq_zero_of_degree_lt _
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : degree (↑f P) = 0 ∧ degree (↑f Q) = 0
⊢ degree (↑f P) < ↑n
[PROOFSTEP]
rw [hPQ.1]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : degree (↑f P) = 0 ∧ degree (↑f Q) = 0
⊢ 0 < ↑n
[PROOFSTEP]
exact (@WithBot.coe_pos _ _ _ n).2 (Ne.bot_lt hn)
[GOAL]
case intro.right
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : degree (↑f P) = 0 ∧ degree (↑f Q) = 0
hcoeff : coeff (↑f P) n = 0
⊢ coeff P n ∈ I
[PROOFSTEP]
rw [coe_mapRingHom, coeff_map, ← RingHom.mem_ker, Ideal.mk_ker] at hcoeff
[GOAL]
case intro.right
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : degree (↑f P) = 0 ∧ degree (↑f Q) = 0
hcoeff : coeff P n ∈ I
⊢ coeff P n ∈ I
[PROOFSTEP]
exact hcoeff
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ IsUnit (↑C r + X * P) ↔ IsUnit r ∧ IsNilpotent P
[PROOFSTEP]
have : ∀ i, coeff (C r + X * P) (i + 1) = coeff P i := by simp
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ ∀ (i : ℕ), coeff (↑C r + X * P) (i + 1) = coeff P i
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : ∀ (i : ℕ), coeff (↑C r + X * P) (i + 1) = coeff P i
⊢ IsUnit (↑C r + X * P) ↔ IsUnit r ∧ IsNilpotent P
[PROOFSTEP]
simp_rw [isUnit_iff_coeff_isUnit_isNilpotent, Nat.forall_ne_zero_iff, this]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : ∀ (i : ℕ), coeff (↑C r + X * P) (i + 1) = coeff P i
⊢ (IsUnit (coeff (↑C r + X * P) 0) ∧ ∀ (i : ℕ), IsNilpotent (coeff P i)) ↔ IsUnit r ∧ IsNilpotent P
[PROOFSTEP]
simp only [coeff_add, coeff_C_zero, mul_coeff_zero, coeff_X_zero, zero_mul, add_zero, and_congr_right_iff, ←
  Polynomial.isNilpotent_iff]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
[PROOFSTEP]
suffices : P = C (eval 0 P) + X * (P /ₘ X)
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : P = ↑C (eval 0 P) + X * (P /ₘ X)
⊢ IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
[PROOFSTEP]
conv_lhs => rw [this]; simp
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : P = ↑C (eval 0 P) + X * (P /ₘ X)
| IsUnit P
[PROOFSTEP]
rw [this]; simp
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : P = ↑C (eval 0 P) + X * (P /ₘ X)
| IsUnit P
[PROOFSTEP]
rw [this]; simp
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : P = ↑C (eval 0 P) + X * (P /ₘ X)
| IsUnit P
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : P = ↑C (eval 0 P) + X * (P /ₘ X)
| IsUnit (↑C (eval 0 P) + X * (P /ₘ X))
[PROOFSTEP]
simp
[GOAL]
case this
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ P = ↑C (eval 0 P) + X * (P /ₘ X)
[PROOFSTEP]
conv_lhs => rw [← modByMonic_add_div P monic_X]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
| P
[PROOFSTEP]
rw [← modByMonic_add_div P monic_X]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
| P
[PROOFSTEP]
rw [← modByMonic_add_div P monic_X]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
| P
[PROOFSTEP]
rw [← modByMonic_add_div P monic_X]
[GOAL]
case this
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ P %ₘ X + X * (P /ₘ X) = ↑C (eval 0 P) + X * (P /ₘ X)
[PROOFSTEP]
simp [modByMonic_X]


[GOAL]
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
⊢ { x_1 // x_1 ∈ Algebra.adjoin F {x} } ≃ₐ[F] AdjoinRoot (minpoly F x)
[PROOFSTEP]
refine AlgEquiv.symm ?_
[GOAL]
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
⊢ AdjoinRoot (minpoly F x) ≃ₐ[F] { x_1 // x_1 ∈ Algebra.adjoin F {x} }
[PROOFSTEP]
refine AlgEquiv.ofBijective (AlgHom.codRestrict (AdjoinRoot.liftHom _ x <| minpoly.aeval F x) _ fun p => ?_) ⟨?_, ?_⟩
[GOAL]
case refine_1
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : AdjoinRoot (minpoly F x)
⊢ ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) p ∈ Algebra.adjoin F {x}
[PROOFSTEP]
induction p using AdjoinRoot.induction_on with
| ih p => exact (Algebra.adjoin_singleton_eq_range_aeval F x).symm ▸ (Polynomial.aeval _).mem_range.mpr ⟨p, rfl⟩
[GOAL]
case refine_1
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : AdjoinRoot (minpoly F x)
⊢ ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) p ∈ Algebra.adjoin F {x}
[PROOFSTEP]
induction p using AdjoinRoot.induction_on with
| ih p => exact (Algebra.adjoin_singleton_eq_range_aeval F x).symm ▸ (Polynomial.aeval _).mem_range.mpr ⟨p, rfl⟩
[GOAL]
case refine_1.ih
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : F[X]
⊢ ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (↑(AdjoinRoot.mk (minpoly F x)) p) ∈
    Algebra.adjoin F {x}
[PROOFSTEP]

| ih p => exact (Algebra.adjoin_singleton_eq_range_aeval F x).symm ▸ (Polynomial.aeval _).mem_range.mpr ⟨p, rfl⟩
[GOAL]
case refine_1.ih
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : F[X]
⊢ ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (↑(AdjoinRoot.mk (minpoly F x)) p) ∈
    Algebra.adjoin F {x}
[PROOFSTEP]
exact (Algebra.adjoin_singleton_eq_range_aeval F x).symm ▸ (Polynomial.aeval _).mem_range.mpr ⟨p, rfl⟩
[GOAL]
case refine_2
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
⊢ Function.Injective
    ↑(AlgHom.codRestrict (AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (Algebra.adjoin F {x})
        (_ :
          ∀ (p : AdjoinRoot (minpoly F x)),
            ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) p ∈ Algebra.adjoin F {x}))
[PROOFSTEP]
apply (AlgHom.injective_codRestrict _ _ _).2
[GOAL]
case refine_2
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
⊢ Function.Injective ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0))
[PROOFSTEP]
apply (injective_iff_map_eq_zero _).2
[GOAL]
case refine_2
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
⊢ ∀ (a : AdjoinRoot (minpoly F x)),
    ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) a = 0 → a = 0
[PROOFSTEP]
intro p
[GOAL]
case refine_2
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : AdjoinRoot (minpoly F x)
⊢ ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) p = 0 → p = 0
[PROOFSTEP]
induction p using AdjoinRoot.induction_on with
| ih p =>
  intro hp
  apply Ideal.Quotient.eq_zero_iff_mem.2
  apply Ideal.mem_span_singleton.2
  apply minpoly.dvd F x hp
[GOAL]
case refine_2
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : AdjoinRoot (minpoly F x)
⊢ ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) p = 0 → p = 0
[PROOFSTEP]
induction p using AdjoinRoot.induction_on with
| ih p =>
  intro hp
  apply Ideal.Quotient.eq_zero_iff_mem.2
  apply Ideal.mem_span_singleton.2
  apply minpoly.dvd F x hp
[GOAL]
case refine_2.ih
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : F[X]
⊢ ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (↑(AdjoinRoot.mk (minpoly F x)) p) = 0 →
    ↑(AdjoinRoot.mk (minpoly F x)) p = 0
[PROOFSTEP]

| ih p =>
  intro hp
  apply Ideal.Quotient.eq_zero_iff_mem.2
  apply Ideal.mem_span_singleton.2
  apply minpoly.dvd F x hp
[GOAL]
case refine_2.ih
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : F[X]
⊢ ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (↑(AdjoinRoot.mk (minpoly F x)) p) = 0 →
    ↑(AdjoinRoot.mk (minpoly F x)) p = 0
[PROOFSTEP]
intro hp
[GOAL]
case refine_2.ih
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : F[X]
hp : ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (↑(AdjoinRoot.mk (minpoly F x)) p) = 0
⊢ ↑(AdjoinRoot.mk (minpoly F x)) p = 0
[PROOFSTEP]
apply Ideal.Quotient.eq_zero_iff_mem.2
[GOAL]
case refine_2.ih
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : F[X]
hp : ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (↑(AdjoinRoot.mk (minpoly F x)) p) = 0
⊢ p ∈ Ideal.span {minpoly F x}
[PROOFSTEP]
apply Ideal.mem_span_singleton.2
[GOAL]
case refine_2.ih
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
p : F[X]
hp : ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (↑(AdjoinRoot.mk (minpoly F x)) p) = 0
⊢ minpoly F x ∣ p
[PROOFSTEP]
apply minpoly.dvd F x hp
[GOAL]
case refine_3
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
⊢ Function.Surjective
    ↑(AlgHom.codRestrict (AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (Algebra.adjoin F {x})
        (_ :
          ∀ (p : AdjoinRoot (minpoly F x)),
            ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) p ∈ Algebra.adjoin F {x}))
[PROOFSTEP]
intro y
[GOAL]
case refine_3
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
y : { x_1 // x_1 ∈ Algebra.adjoin F {x} }
⊢ ∃ a,
    ↑(AlgHom.codRestrict (AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (Algebra.adjoin F {x})
            (_ :
              ∀ (p : AdjoinRoot (minpoly F x)),
                ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) p ∈ Algebra.adjoin F {x}))
        a =
      y
[PROOFSTEP]
let ⟨p, hp⟩ := (SetLike.ext_iff.1 (Algebra.adjoin_singleton_eq_range_aeval F x) (y : R)).1 y.2
[GOAL]
case refine_3
F : Type u_1
inst✝² : Field F
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Algebra F R
x : R
y : { x_1 // x_1 ∈ Algebra.adjoin F {x} }
p : F[X]
hp : ↑↑(aeval x) p = ↑y
⊢ ∃ a,
    ↑(AlgHom.codRestrict (AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) (Algebra.adjoin F {x})
            (_ :
              ∀ (p : AdjoinRoot (minpoly F x)),
                ↑(AdjoinRoot.liftHom (minpoly F x) x (_ : ↑(aeval x) (minpoly F x) = 0)) p ∈ Algebra.adjoin F {x}))
        a =
      y
[PROOFSTEP]
exact ⟨AdjoinRoot.mk _ p, Subtype.eq hp⟩
[GOAL]
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s : Finset K
⊢ (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
[PROOFSTEP]
classical
refine' Finset.induction_on s (fun _ => _) fun a s _ ih H => _
· rw [coe_empty, Algebra.adjoin_empty]
  exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩
rw [forall_mem_insert] at H
rcases H with ⟨⟨H1, H2⟩, H3⟩
cases' ih H3 with f
choose H3 _ using H3
rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]
letI := (f : Algebra.adjoin F (↑s : Set K) →+* L).toAlgebra
haveI : FiniteDimensional F (Algebra.adjoin F (↑s : Set K)) :=
  ((Submodule.fg_iff_finiteDimensional _).1 (FG_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule
letI := fieldOfFiniteDimensional F (Algebra.adjoin F (↑s : Set K))
have H5 : IsIntegral (Algebra.adjoin F (s : Set K)) a := isIntegral_of_isScalarTower H1
have H6 : (minpoly (Algebra.adjoin F (s : Set K)) a).Splits (algebraMap (Algebra.adjoin F (s : Set K)) L) :=
  by
  have : Polynomial.map (algebraMap F (Algebra.adjoin F (s : Set K))) (minpoly F a) ≠ 0 :=
    Polynomial.map_ne_zero <| minpoly.ne_zero H1
  refine' Polynomial.splits_of_splits_of_dvd _ this ((Polynomial.splits_map_iff _ _).2 _) (minpoly.dvd _ _ _)
  · rw [← IsScalarTower.algebraMap_eq]
    exact H2
  · rw [Polynomial.aeval_map_algebraMap, minpoly.aeval]
obtain ⟨y, hy⟩ := Polynomial.exists_root_of_splits _ H6 (ne_of_lt (minpoly.degree_pos H5)).symm
refine' ⟨Subalgebra.ofRestrictScalars F _ _⟩
refine' (AdjoinRoot.liftHom (minpoly (Algebra.adjoin F (↑s : Set K)) a) y hy).comp _
exact (AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly (Algebra.adjoin F (↑s : Set K)) a).toAlgHom
[GOAL]
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s : Finset K
⊢ (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
[PROOFSTEP]
refine' Finset.induction_on s (fun _ => _) fun a s _ ih H => _
[GOAL]
case refine'_1
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s : Finset K
x✝ : ∀ (x : K), x ∈ ∅ → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑∅ } →ₐ[F] L)
[PROOFSTEP]
rw [coe_empty, Algebra.adjoin_empty]
[GOAL]
case refine'_1
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s : Finset K
x✝ : ∀ (x : K), x ∈ ∅ → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ ⊥ } →ₐ[F] L)
[PROOFSTEP]
exact ⟨(Algebra.ofId F L).comp (Algebra.botEquiv F K)⟩
[GOAL]
case refine'_2
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H : ∀ (x : K), x ∈ insert a s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑(insert a s) } →ₐ[F] L)
[PROOFSTEP]
rw [forall_mem_insert] at H
[GOAL]
case refine'_2
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H :
  (IsIntegral F a ∧ Splits (algebraMap F L) (minpoly F a)) ∧
    ∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑(insert a s) } →ₐ[F] L)
[PROOFSTEP]
rcases H with ⟨⟨H1, H2⟩, H3⟩
[GOAL]
case refine'_2.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H3 : ∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑(insert a s) } →ₐ[F] L)
[PROOFSTEP]
cases' ih H3 with f
[GOAL]
case refine'_2.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H3 : ∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑(insert a s) } →ₐ[F] L)
[PROOFSTEP]
choose H3 _ using H3
[GOAL]
case refine'_2.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ Algebra.adjoin F ↑(insert a s) } →ₐ[F] L)
[PROOFSTEP]
rw [coe_insert, Set.insert_eq, Set.union_comm, Algebra.adjoin_union_eq_adjoin_adjoin]
[GOAL]
case refine'_2.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
[PROOFSTEP]
letI := (f : Algebra.adjoin F (↑s : Set K) →+* L).toAlgebra
[GOAL]
case refine'_2.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
[PROOFSTEP]
haveI : FiniteDimensional F (Algebra.adjoin F (↑s : Set K)) :=
  ((Submodule.fg_iff_finiteDimensional _).1 (FG_adjoin_of_finite s.finite_toSet H3)).of_subalgebra_toSubmodule
[GOAL]
case refine'_2.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
[PROOFSTEP]
letI := fieldOfFiniteDimensional F (Algebra.adjoin F (↑s : Set K))
[GOAL]
case refine'_2.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
[PROOFSTEP]
have H5 : IsIntegral (Algebra.adjoin F (s : Set K)) a := isIntegral_of_isScalarTower H1
[GOAL]
case refine'_2.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
[PROOFSTEP]
have H6 : (minpoly (Algebra.adjoin F (s : Set K)) a).Splits (algebraMap (Algebra.adjoin F (s : Set K)) L) :=
  by
  have : Polynomial.map (algebraMap F (Algebra.adjoin F (s : Set K))) (minpoly F a) ≠ 0 :=
    Polynomial.map_ne_zero <| minpoly.ne_zero H1
  refine' Polynomial.splits_of_splits_of_dvd _ this ((Polynomial.splits_map_iff _ _).2 _) (minpoly.dvd _ _ _)
  · rw [← IsScalarTower.algebraMap_eq]
    exact H2
  · rw [Polynomial.aeval_map_algebraMap, minpoly.aeval]
[GOAL]
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
⊢ Splits (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
[PROOFSTEP]
have : Polynomial.map (algebraMap F (Algebra.adjoin F (s : Set K))) (minpoly F a) ≠ 0 :=
  Polynomial.map_ne_zero <| minpoly.ne_zero H1
[GOAL]
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝² : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝¹ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this✝ : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
this : Polynomial.map (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }) (minpoly F a) ≠ 0
⊢ Splits (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
[PROOFSTEP]
refine' Polynomial.splits_of_splits_of_dvd _ this ((Polynomial.splits_map_iff _ _).2 _) (minpoly.dvd _ _ _)
[GOAL]
case refine'_1
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝² : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝¹ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this✝ : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
this : Polynomial.map (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }) (minpoly F a) ≠ 0
⊢ Splits (RingHom.comp (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }))
    (minpoly F a)
[PROOFSTEP]
rw [← IsScalarTower.algebraMap_eq]
[GOAL]
case refine'_1
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝² : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝¹ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this✝ : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
this : Polynomial.map (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }) (minpoly F a) ≠ 0
⊢ Splits (algebraMap F L) (minpoly F a)
[PROOFSTEP]
exact H2
[GOAL]
case refine'_2
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝² : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝¹ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this✝ : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
this : Polynomial.map (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }) (minpoly F a) ≠ 0
⊢ ↑(aeval a) (Polynomial.map (algebraMap F { x // x ∈ Algebra.adjoin F ↑s }) (minpoly F a)) = 0
[PROOFSTEP]
rw [Polynomial.aeval_map_algebraMap, minpoly.aeval]
[GOAL]
case refine'_2.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
H6 : Splits (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
[PROOFSTEP]
obtain ⟨y, hy⟩ := Polynomial.exists_root_of_splits _ H6 (ne_of_lt (minpoly.degree_pos H5)).symm
[GOAL]
case refine'_2.intro.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
H6 : Splits (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
y : L
hy : eval₂ (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) y (minpoly { x // x ∈ Algebra.adjoin F ↑s } a) = 0
⊢ Nonempty ({ x // x ∈ Subalgebra.restrictScalars F (Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a}) } →ₐ[F] L)
[PROOFSTEP]
refine' ⟨Subalgebra.ofRestrictScalars F _ _⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
H6 : Splits (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
y : L
hy : eval₂ (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) y (minpoly { x // x ∈ Algebra.adjoin F ↑s } a) = 0
⊢ { x // x ∈ Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a} } →ₐ[{ x // x ∈ Algebra.adjoin F ↑s }] L
[PROOFSTEP]
refine' (AdjoinRoot.liftHom (minpoly (Algebra.adjoin F (↑s : Set K)) a) y hy).comp _
[GOAL]
case refine'_2.intro.intro.intro.intro
F✝ : Type u_1
inst✝⁵ : Field F✝
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : ¬a ∈ s
ih :
  (∀ (x : K), x ∈ s → IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) →
    Nonempty ({ x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L)
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
f : { x // x ∈ Algebra.adjoin F ↑s } →ₐ[F] L
H3 : ∀ (x : K), x ∈ s → IsIntegral F x
✝ : ∀ (x : K), x ∈ s → Splits (algebraMap F L) (minpoly F x)
this✝¹ : Algebra { x // x ∈ Algebra.adjoin F ↑s } L := RingHom.toAlgebra ↑f
this✝ : FiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
this : Field { x // x ∈ Algebra.adjoin F ↑s } := fieldOfFiniteDimensional F { x // x ∈ Algebra.adjoin F ↑s }
H5 : IsIntegral { x // x ∈ Algebra.adjoin F ↑s } a
H6 : Splits (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
y : L
hy : eval₂ (algebraMap { x // x ∈ Algebra.adjoin F ↑s } L) y (minpoly { x // x ∈ Algebra.adjoin F ↑s } a) = 0
⊢ { x // x ∈ Algebra.adjoin { x // x ∈ Algebra.adjoin F ↑s } {a} } →ₐ[{ x // x ∈ Algebra.adjoin F ↑s }]
    AdjoinRoot (minpoly { x // x ∈ Algebra.adjoin F ↑s } a)
[PROOFSTEP]
exact (AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly (Algebra.adjoin F (↑s : Set K)) a).toAlgHom