-- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
lemma coeff_minpolyDiv_mem_adjoin (x : S) (i) :
    coeff (minpolyDiv R x) i ∈ Algebra.adjoin R {x}

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
⊢ i + (minpolyDiv R x).natDegree < i + ((minpolyDiv R x).natDegree + 1)

Tactic:
rw [← add_assoc]

Result:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
⊢ i + (minpolyDiv R x).natDegree < i + (minpolyDiv R x).natDegree + 1

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
⊢ (minpolyDiv R x).coeff (i + ((minpolyDiv R x).natDegree + 1)) ∈ Algebra.adjoin R {x}

Tactic:
rw [coeff_eq_zero_of_natDegree_lt]

Result:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
⊢ 0 ∈ Algebra.adjoin R {x}

R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
⊢ (minpolyDiv R x).natDegree < i + ((minpolyDiv R x).natDegree + 1)

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
⊢ i + (minpolyDiv R x).natDegree < i + (minpolyDiv R x).natDegree + 1

Tactic:
exact Nat.lt_succ_self _

Result:
no goals

Proof state:
case zero
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
⊢ (minpolyDiv R x).coeff (i + 0) ∉ Algebra.adjoin R {x}

Tactic:
exact H

Result:
no goals

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
⊢ (minpolyDiv R x).coeff i ∈ Algebra.adjoin R {x}

Tactic:
by_contra H

Result:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
⊢ False

Proof state:
case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H✝ : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
j : ℕ
IH : (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
H : (minpolyDiv R x).coeff (i + (j + 1)) ∈ Algebra.adjoin R {x}
⊢ False

Tactic:
apply IH

Result:
case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H✝ : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
j : ℕ
IH : (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
H : (minpolyDiv R x).coeff (i + (j + 1)) ∈ Algebra.adjoin R {x}
⊢ (minpolyDiv R x).coeff (i + j) ∈ Algebra.adjoin R {x}

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
⊢ 0 ∈ Algebra.adjoin R {x}

Tactic:
exact zero_mem _

Result:
no goals

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
⊢ False

Tactic:
apply this (natDegree (minpolyDiv R x) + 1)

Result:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
⊢ (minpolyDiv R x).coeff (i + ((minpolyDiv R x).natDegree + 1)) ∈ Algebra.adjoin R {x}

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
⊢ (minpolyDiv R x).natDegree < i + ((minpolyDiv R x).natDegree + 1)

Tactic:
refine (Nat.le_add_left _ i).trans_lt ?_

Result:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
this : ∀ (j : ℕ), (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
⊢ i + (minpolyDiv R x).natDegree < i + ((minpolyDiv R x).natDegree + 1)

Proof state:
case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
j : ℕ
IH : (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
⊢ (minpolyDiv R x).coeff (i + (j + 1)) ∉ Algebra.adjoin R {x}

Tactic:
intro H

Result:
case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H✝ : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
j : ℕ
IH : (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
H : (minpolyDiv R x).coeff (i + (j + 1)) ∈ Algebra.adjoin R {x}
⊢ False

Proof state:
case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H✝ : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
j : ℕ
IH : (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
H : (minpolyDiv R x).coeff (i + (j + 1)) ∈ Algebra.adjoin R {x}
⊢ (algebraMap R S) ((minpoly R x).coeff (i + j + 1)) + (minpolyDiv R x).coeff (i + j + 1) * x ∈ Algebra.adjoin R {x}

Tactic:
refine add_mem ?_ (mul_mem H (Algebra.self_mem_adjoin_singleton R x))

Result:
case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H✝ : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
j : ℕ
IH : (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
H : (minpolyDiv R x).coeff (i + (j + 1)) ∈ Algebra.adjoin R {x}
⊢ (algebraMap R S) ((minpoly R x).coeff (i + j + 1)) ∈ Algebra.adjoin R {x}

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
j : ℕ
⊢ (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}

Tactic:
induction j with
| zero => exact H
| succ j IH =>
intro H; apply IH
rw [coeff_minpolyDiv]
refine add_mem ?_ (mul_mem H (Algebra.self_mem_adjoin_singleton R x))
exact Subalgebra.algebraMap_mem _ _

Result:
no goals

Proof state:
case succ
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
i : ℕ
H✝ : (minpolyDiv R x).coeff i ∉ Algebra.adjoin R {x}
j : ℕ
IH : (minpolyDiv R x).coeff (i + j) ∉ Algebra.adjoin R {x}
H : (minpolyDiv R x).coeff (i + (j + 1)) ∈ Algebra.adjoin R {x}
⊢ (algebraMap R S) ((minpoly R x).coeff (i + j + 1)) ∈ Algebra.adjoin R {x}

Tactic:
exact Subalgebra.algebraMap_mem _ _

Result:
no goals