-- Mathlib/RingTheory/PowerBasis.lean
theorem mem_span_pow {x y : S} {d : ℕ} (hd : d ≠ 0) :
    y ∈ Submodule.span R (Set.range fun i : Fin d => x ^ (i : ℕ)) ↔
      ∃ f : R[X], f.natDegree < d ∧ y = aeval x f

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
⊢ y ∈ Submodule.span R (Set.range fun i => x ^ ↑i) ↔ ∃ f, f.natDegree < d ∧ y = (aeval x) f

Tactic:
rw [mem_span_pow']

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
⊢ (∃ f, f.degree < ↑d ∧ y = (aeval x) f) ↔ ∃ f, f.natDegree < d ∧ y = (aeval x) f

Proof state:
case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = (aeval x) f
hf : f = 0
h : 0 < d
⊢ ⊥ < ↑d

Tactic:
exact WithBot.bot_lt_coe d

Result:
no goals

Proof state:
case mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
⊢ f.degree < ↑d

Tactic:
by_cases hf : f = 0

Result:
case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
hf : f = 0
⊢ f.degree < ↑d

case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
hf : ¬f = 0
⊢ f.degree < ↑d

Proof state:
case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : ↑f.natDegree < ↑d
hy : y = (aeval x) f
hf : ¬f = 0
⊢ f.natDegree < d

Tactic:
exact WithBot.coe_lt_coe.1 h

Result:
no goals

Proof state:
case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
hf : ¬f = 0
⊢ ↑f.natDegree < ↑d

Tactic:
exact WithBot.coe_lt_coe.2 h

Result:
no goals

Proof state:
case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
hf : f = 0
⊢ f.degree < ↑d

Tactic:
simp only [hf, natDegree_zero, degree_zero] at h ⊢

Result:
case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = (aeval x) f
hf : f = 0
h : 0 < d
⊢ ⊥ < ↑d

Proof state:
case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = (aeval x) f
hf : f = 0
h : ⊥ < ↑d
⊢ 0 < d

Tactic:
exact lt_of_le_of_ne (Nat.zero_le d) hd.symm

Result:
no goals

Proof state:
case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
hf : ¬f = 0
⊢ f.degree < ↑d

Tactic:
simp_all only [degree_eq_natDegree hf]

Result:
case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
hf : ¬f = 0
⊢ ↑f.natDegree < ↑d

Proof state:
case neg
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
hf : ¬f = 0
⊢ ↑f.natDegree < ↑d

Tactic:
first | exact WithBot.coe_lt_coe.1 h | exact WithBot.coe_lt_coe.2 h

Result:
no goals

Proof state:
case pos
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
hy : y = (aeval x) f
hf : f = 0
h : 0 < d
⊢ ⊥ < ↑d

Tactic:
first | exact lt_of_le_of_ne (Nat.zero_le d) hd.symm | exact WithBot.bot_lt_coe d

Result:
no goals

Proof state:
case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
⊢ (∃ f, f.natDegree < d ∧ y = (aeval x) f) → ∃ f, f.degree < ↑d ∧ y = (aeval x) f

Tactic:
rintro ⟨f, h, hy⟩

Result:
case mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
⊢ ∃ f, f.degree < ↑d ∧ y = (aeval x) f

Proof state:
case mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
⊢ ∃ f, f.degree < ↑d ∧ y = (aeval x) f

Tactic:
refine ⟨f, ?_, hy⟩

Result:
case mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x y : S
d : ℕ
hd : d ≠ 0
f : R[X]
h : f.natDegree < d
hy : y = (aeval x) f
⊢ f.degree < ↑d