case refine'_1
K : Type u_2
L : Type u_3
L' : Type ?u.178908
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P f g : R[X]
hf : ↑(aeval ↑x) f = ↑(↑(aeval x) f)
hg : ↑(aeval ↑x) g = ↑(↑(aeval x) g)
⊢ ↑(aeval ↑x) (f + g) = ↑(↑(aeval x) (f + g))

case refine'_2
K : Type u_2
L : Type u_3
L' : Type ?u.178908
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
n : ℕ
r : R
⊢ ↑(aeval ↑x) (↑(monomial n) r) = ↑(↑(aeval x) (↑(monomial n) r))
K : Type u_2
L : Type u_3
L' : Type ?u.178908
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
⊢ ↑(aeval ↑x) P = ↑(↑(aeval x) P)
refine' Polynomial.induction_on' P (fun f g hf hg => _) fun n r => _
no goals
case refine'_1
K : Type u_2
L : Type u_3
L' : Type ?u.178908
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P f g : R[X]
hf : ↑(aeval ↑x) f = ↑(↑(aeval x) f)
hg : ↑(aeval ↑x) g = ↑(↑(aeval x) g)
⊢ ↑(aeval ↑x) (f + g) = ↑(↑(aeval x) (f + g))
rw [aeval_add, aeval_add, AddMemClass.coe_add, hf, hg]
case refine'_2
K : Type u_2
L : Type u_3
L' : Type ?u.178908
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
n : ℕ
r : R
⊢ ↑(algebraMap R L) r = ↑(↑(algebraMap R { x // x ∈ S }) r) ∨ ↑x ^ n = 0
case refine'_2
K : Type u_2
L : Type u_3
L' : Type ?u.178908
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
n : ℕ
r : R
⊢ ↑(aeval ↑x) (↑(monomial n) r) = ↑(↑(aeval x) (↑(monomial n) r))
simp only [MulMemClass.coe_mul, aeval_monomial, SubmonoidClass.coe_pow, mul_eq_mul_right_iff]
case refine'_2.h
K : Type u_2
L : Type u_3
L' : Type ?u.178908
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
n : ℕ
r : R
⊢ ↑(algebraMap R L) r = ↑(↑(algebraMap R { x // x ∈ S }) r)
case refine'_2
K : Type u_2
L : Type u_3
L' : Type ?u.178908
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
n : ℕ
r : R
⊢ ↑(algebraMap R L) r = ↑(↑(algebraMap R { x // x ∈ S }) r) ∨ ↑x ^ n = 0
left
no goals
case refine'_2.h
K : Type u_2
L : Type u_3
L' : Type ?u.178908
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
n : ℕ
r : R
⊢ ↑(algebraMap R L) r = ↑(↑(algebraMap R { x // x ∈ S }) r)
rfl