R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.28630
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
⊢ (∃ f, degree f < ↑d ∧ y = ↑(aeval x) f) ↔ ∃ f, natDegree f < d ∧ y = ↑(aeval x) f
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.28630
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
⊢ y ∈ Submodule.span R (Set.range fun i => x ^ ↑i) ↔ ∃ f, natDegree f < d ∧ y = ↑(aeval x) f
rw [mem_span_pow']
case mpr.intro.intro
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.28630
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : natDegree f < d
hy : y = ↑(aeval x) f
⊢ ∃ f, degree f < ↑d ∧ y = ↑(aeval x) f
case mpr
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.28630
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
⊢ (∃ f, natDegree f < d ∧ y = ↑(aeval x) f) → ∃ f, degree f < ↑d ∧ y = ↑(aeval x) f
rintro ⟨f, h, hy⟩
case mpr.intro.intro
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.28630
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : natDegree f < d
hy : y = ↑(aeval x) f
⊢ degree f < ↑d
case mpr.intro.intro
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.28630
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : natDegree f < d
hy : y = ↑(aeval x) f
⊢ ∃ f, degree f < ↑d ∧ y = ↑(aeval x) f
refine' ⟨f, _, hy⟩
case pos
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.28630
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : natDegree f < d
hy : y = ↑(aeval x) f
hf : f = 0
⊢ degree f < ↑d

case neg
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.28630
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : natDegree f < d
hy : y = ↑(aeval x) f
hf : ¬f = 0
⊢ degree f < ↑d
case mpr.intro.intro
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.28630
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : natDegree f < d
hy : y = ↑(aeval x) f
⊢ degree f < ↑d
by_cases hf : f = 0
case neg
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
K : Type ?u.28630
inst✝¹ : Field K
x y : S
d : ℕ
f : R[X]
inst✝ : IsDomain B
hd : d ≠ 0
h : natDegree f < d
hy : y = ↑(aeval x) f
hf : ¬f = 0
⊢ ↑(natDegree f) < ↑d
case neg
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.28630
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : natDegree f < d
hy : y = ↑(aeval x) f
hf : ¬f = 0
⊢ degree f < ↑d
simp_all only [degree_eq_natDegree hf]
case pos
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.28630
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = ↑(aeval x) f
hf : f = 0
h : 0 < d
⊢ ⊥ < ↑d
case pos
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.28630
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : natDegree f < d
hy : y = ↑(aeval x) f
hf : f = 0
⊢ degree f < ↑d
simp only [hf, natDegree_zero, degree_zero] at h⊢
no goals
case pos
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.28630
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = ↑(aeval x) f
hf : f = 0
h : 0 < d
⊢ ⊥ < ↑d
first | exact lt_of_le_of_ne (Nat.zero_le d) hd.symm | exact WithBot.bot_lt_coe d
case pos
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.28630
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = ↑(aeval x) f
hf : f = 0
h : 0 < d
⊢ ⊥ < ↑d
case pos
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.28630
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = ↑(aeval x) f
hf : f = 0
h : 0 < d
⊢ ⊥ < ↑d
exact lt_of_le_of_ne (Nat.zero_le d) hd.symm
no goals
case pos
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : IsDomain B
inst✝¹ : Algebra A B
K : Type ?u.28630
inst✝ : Field K
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = ↑(aeval x) f
hf : f = 0
h : 0 < d
⊢ ⊥ < ↑d
exact WithBot.bot_lt_coe d
no goals
case neg
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
K : Type ?u.28630
inst✝¹ : Field K
x y : S
d : ℕ
f : R[X]
inst✝ : IsDomain B
hd : d ≠ 0
h : natDegree f < d
hy : y = ↑(aeval x) f
hf : ¬f = 0
⊢ ↑(natDegree f) < ↑d
first | exact WithBot.coe_lt_coe.1 h | exact WithBot.coe_lt_coe.2 h
case neg
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
K : Type ?u.28630
inst✝¹ : Field K
x y : S
d : ℕ
f : R[X]
inst✝ : IsDomain B
hd : d ≠ 0
h : natDegree f < d
hy : y = ↑(aeval x) f
hf : ¬f = 0
⊢ ↑(natDegree f) < ↑d
case neg
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
K : Type ?u.28630
inst✝¹ : Field K
x y : S
d : ℕ
f : R[X]
inst✝ : IsDomain B
hd : d ≠ 0
h : natDegree f < d
hy : y = ↑(aeval x) f
hf : ¬f = 0
⊢ ↑(natDegree f) < ↑d
exact WithBot.coe_lt_coe.1 h
no goals
case neg
R : Type u_2
S : Type u_1
T : Type ?u.27902
inst✝⁷ : CommRing R
inst✝⁶ : Ring S
inst✝⁵ : Algebra R S
A : Type ?u.28205
B : Type ?u.28208
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
K : Type ?u.28630
inst✝¹ : Field K
x y : S
d : ℕ
f : R[X]
inst✝ : IsDomain B
hd : d ≠ 0
h : natDegree f < d
hy : y = ↑(aeval x) f
hf : ¬f = 0
⊢ ↑(natDegree f) < ↑d
exact WithBot.coe_lt_coe.2 h