case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
⊢ Ideal.FG (RingHom.ker ↑f)
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
hfp : FinitePresentation R A
⊢ Ideal.FG (RingHom.ker ↑f)
obtain ⟨m, f', hf', s, hs⟩ := hfp
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
⊢ Ideal.FG (RingHom.ker ↑f)
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
⊢ Ideal.FG (RingHom.ker ↑f)
let RXn := MvPolynomial (Fin n) R
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
⊢ Ideal.FG (RingHom.ker ↑f)
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
⊢ Ideal.FG (RingHom.ker ↑f)
let RXm := MvPolynomial (Fin m) R
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
this : ∀ (i : Fin n), ∃ a, ↑f' a = ↑f (MvPolynomial.X i)
⊢ Ideal.FG (RingHom.ker ↑f)
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
⊢ Ideal.FG (RingHom.ker ↑f)
have := fun i : Fin n => hf' (f <| X i)
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
⊢ Ideal.FG (RingHom.ker ↑f)
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
this : ∀ (i : Fin n), ∃ a, ↑f' a = ↑f (MvPolynomial.X i)
⊢ Ideal.FG (RingHom.ker ↑f)
choose g hg using this
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
this : ∀ (i : Fin m), ∃ a, ↑f a = ↑f' (MvPolynomial.X i)
⊢ Ideal.FG (RingHom.ker ↑f)
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
⊢ Ideal.FG (RingHom.ker ↑f)
have := fun i : Fin m => hf (f' <| X i)
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
⊢ Ideal.FG (RingHom.ker ↑f)
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
this : ∀ (i : Fin m), ∃ a, ↑f a = ↑f' (MvPolynomial.X i)
⊢ Ideal.FG (RingHom.ker ↑f)
choose h hh using this
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
⊢ Ideal.FG (RingHom.ker ↑f)
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
⊢ Ideal.FG (RingHom.ker ↑f)
let aeval_h : RXm →ₐ[R] RXn := aeval h
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
⊢ Ideal.FG (RingHom.ker ↑f)
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
⊢ Ideal.FG (RingHom.ker ↑f)
let g' : Fin n → RXn := fun i => X i - aeval_h (g i)
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
⊢ Ideal.span ↑(Finset.image g' Finset.univ ∪ Finset.image (↑aeval_h) s) = RingHom.ker ↑f
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
⊢ Ideal.FG (RingHom.ker ↑f)
refine' ⟨Finset.univ.image g' ∪ s.image aeval_h, _⟩
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
⊢ Ideal.span ((Set.range fun i => MvPolynomial.X i - ↑(MvPolynomial.aeval h) (g i)) ∪ ↑(MvPolynomial.aeval h) '' ↑s) =
    RingHom.ker ↑f
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
⊢ Ideal.span ↑(Finset.image g' Finset.univ ∪ Finset.image (↑aeval_h) s) = RingHom.ker ↑f
simp only [Finset.coe_image, Finset.coe_union, Finset.coe_univ, Set.image_univ]
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
⊢ Ideal.span ((Set.range fun i => MvPolynomial.X i - ↑(MvPolynomial.aeval h) (g i)) ∪ ↑(MvPolynomial.aeval h) '' ↑s) =
    RingHom.ker ↑f
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
⊢ Ideal.span ((Set.range fun i => MvPolynomial.X i - ↑(MvPolynomial.aeval h) (g i)) ∪ ↑(MvPolynomial.aeval h) '' ↑s) =
    RingHom.ker ↑f
have hh' : ∀ x, f (aeval_h x) = f' x := by
  intro x
  rw [← f.coe_toRingHom, map_aeval]
  simp_rw [AlgHom.coe_toRingHom, hh]
  rw [AlgHom.comp_algebraMap, ← aeval_eq_eval₂Hom,
    ← funext fun i => Function.comp_apply (f := ↑f') (g := MvPolynomial.X),
    ← aeval_unique]
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
⊢ Ideal.span ((Set.range fun i => MvPolynomial.X i - ↑(MvPolynomial.aeval h) (g i)) ∪ ↑(MvPolynomial.aeval h) '' ↑s) =
    RingHom.ker ↑f
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
⊢ Ideal.span ((Set.range fun i => MvPolynomial.X i - ↑(MvPolynomial.aeval h) (g i)) ∪ ↑(MvPolynomial.aeval h) '' ↑s) =
    RingHom.ker ↑f
let s' := Set.range g' ∪ aeval_h '' s
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
⊢ RingHom.ker ↑f ≤ Ideal.span s'
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
⊢ Ideal.span ((Set.range fun i => MvPolynomial.X i - ↑(MvPolynomial.aeval h) (g i)) ∪ ↑(MvPolynomial.aeval h) '' ↑s) =
    RingHom.ker ↑f
apply leI.antisymm
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
⊢ x ∈ Ideal.span s'
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
⊢ RingHom.ker ↑f ≤ Ideal.span s'
intro x hx
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
hx : ↑↑aeval_h x + y ∈ RingHom.ker ↑f
this : ↑↑aeval_h x + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ ↑↑aeval_h x + y ∈ Ideal.span s'
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ x ∈ Ideal.span s'
obtain ⟨_, ⟨x, rfl⟩, y, hy, rfl⟩ := AddSubmonoid.mem_sup.mp this
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
hx : ↑↑aeval_h x + y ∈ RingHom.ker ↑f
this : ↑↑aeval_h x + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ ↑↑aeval_h x ∈ Ideal.span s'
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
hx : ↑↑aeval_h x + y ∈ RingHom.ker ↑f
this : ↑↑aeval_h x + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ ↑↑aeval_h x + y ∈ Ideal.span s'
refine' add_mem _ hy
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
this : ↑↑aeval_h x + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
hx : ↑f' x = 0
⊢ ↑↑aeval_h x ∈ Ideal.span s'
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
hx : ↑↑aeval_h x + y ∈ RingHom.ker ↑f
this : ↑↑aeval_h x + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ ↑↑aeval_h x ∈ Ideal.span s'
simp only [RingHom.mem_ker, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, map_add,
  show f y = 0 from leI hy, add_zero, hh'] at hx
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
this : ↑↑aeval_h x + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
hx : ↑f' x = 0
⊢ Ideal.span ↑s ≤ Ideal.comap aeval_h (Ideal.span s')
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
this : ↑↑aeval_h x + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
hx : ↑f' x = 0
⊢ ↑↑aeval_h x ∈ Ideal.span s'
suffices Ideal.span (s : Set RXm) ≤ (Ideal.span s').comap aeval_h by
  apply this
  rwa [hs]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
this : ↑↑aeval_h x + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
hx : ↑f' x = 0
⊢ ↑s ⊆ ↑(Ideal.comap aeval_h (Ideal.span s'))
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
this : ↑↑aeval_h x + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
hx : ↑f' x = 0
⊢ Ideal.span ↑s ≤ Ideal.comap aeval_h (Ideal.span s')
rw [Ideal.span_le]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x✝ : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
this : ↑↑aeval_h x✝ + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
hx✝ : ↑f' x✝ = 0
x : MvPolynomial (Fin m) R
hx : x ∈ ↑s
⊢ x ∈ ↑(Ideal.comap aeval_h (Ideal.span s'))
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
this : ↑↑aeval_h x + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
hx : ↑f' x = 0
⊢ ↑s ⊆ ↑(Ideal.comap aeval_h (Ideal.span s'))
intro x hx
case intro.intro.intro.intro.intro.intro.intro.intro.intro.a
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x✝ : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
this : ↑↑aeval_h x✝ + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
hx✝ : ↑f' x✝ = 0
x : MvPolynomial (Fin m) R
hx : x ∈ ↑s
⊢ ↑aeval_h x ∈ s'
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x✝ : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
this : ↑↑aeval_h x✝ + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
hx✝ : ↑f' x✝ = 0
x : MvPolynomial (Fin m) R
hx : x ∈ ↑s
⊢ x ∈ ↑(Ideal.comap aeval_h (Ideal.span s'))
apply Submodule.subset_span
case intro.intro.intro.intro.intro.intro.intro.intro.intro.a.a
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x✝ : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
this : ↑↑aeval_h x✝ + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
hx✝ : ↑f' x✝ = 0
x : MvPolynomial (Fin m) R
hx : x ∈ ↑s
⊢ ↑aeval_h x ∈ ↑aeval_h '' ↑s
case intro.intro.intro.intro.intro.intro.intro.intro.intro.a
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x✝ : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
this : ↑↑aeval_h x✝ + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
hx✝ : ↑f' x✝ = 0
x : MvPolynomial (Fin m) R
hx : x ∈ ↑s
⊢ ↑aeval_h x ∈ s'
apply Set.mem_union_right
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.a.a
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x✝ : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
this : ↑↑aeval_h x✝ + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
hx✝ : ↑f' x✝ = 0
x : MvPolynomial (Fin m) R
hx : x ∈ ↑s
⊢ ↑aeval_h x ∈ ↑aeval_h '' ↑s
exact Set.mem_image_of_mem _ hx
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
x : RXm
⊢ ↑f (↑aeval_h x) = ↑f' x
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
⊢ ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
intro x
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
x : RXm
⊢ ↑(eval₂Hom (RingHom.comp (↑f) (algebraMap R (MvPolynomial (Fin n) R))) fun i => ↑↑f (h i)) x = ↑f' x
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
x : RXm
⊢ ↑f (↑aeval_h x) = ↑f' x
rw [← f.coe_toRingHom, map_aeval]
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
x : RXm
⊢ ↑(eval₂Hom (RingHom.comp (↑f) (algebraMap R (MvPolynomial (Fin n) R))) fun i => ↑f' (MvPolynomial.X i)) x = ↑f' x
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
x : RXm
⊢ ↑(eval₂Hom (RingHom.comp (↑f) (algebraMap R (MvPolynomial (Fin n) R))) fun i => ↑↑f (h i)) x = ↑f' x
simp_rw [AlgHom.coe_toRingHom, hh]
no goals
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
x : RXm
⊢ ↑(eval₂Hom (RingHom.comp (↑f) (algebraMap R (MvPolynomial (Fin n) R))) fun i => ↑f' (MvPolynomial.X i)) x = ↑f' x
rw [AlgHom.comp_algebraMap, ← aeval_eq_eval₂Hom,
  ← funext fun i => Function.comp_apply (f := ↑f') (g := MvPolynomial.X),
  ← aeval_unique]
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
⊢ s' ⊆ ↑(RingHom.ker ↑f)
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
⊢ Ideal.span s' ≤ RingHom.ker ↑f
rw [Ideal.span_le]
case inl.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
i : Fin n
⊢ g' i ∈ ↑(RingHom.ker ↑f)

case inr.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
x : RXm
hx : x ∈ ↑s
⊢ ↑aeval_h x ∈ ↑(RingHom.ker ↑f)
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
⊢ s' ⊆ ↑(RingHom.ker ↑f)
rintro _ (⟨i, rfl⟩ | ⟨x, hx, rfl⟩)
case inl.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
i : Fin n
⊢ ↑f (g' i) = 0
case inl.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
i : Fin n
⊢ g' i ∈ ↑(RingHom.ker ↑f)
change f (g' i) = 0
no goals
case inl.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
i : Fin n
⊢ ↑f (g' i) = 0
rw [map_sub, ← hg, hh', sub_self]
case inr.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
x : RXm
hx : x ∈ ↑s
⊢ ↑f (↑aeval_h x) = 0
case inr.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
x : RXm
hx : x ∈ ↑s
⊢ ↑aeval_h x ∈ ↑(RingHom.ker ↑f)
change f (aeval_h x) = 0
case inr.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
x : RXm
hx : x ∈ ↑s
⊢ ↑f' x = 0
case inr.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
x : RXm
hx : x ∈ ↑s
⊢ ↑f (↑aeval_h x) = 0
rw [hh']
case inr.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
x : RXm
hx : x ∈ ↑s
⊢ x ∈ RingHom.ker ↑f'
case inr.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
x : RXm
hx : x ∈ ↑s
⊢ ↑f' x = 0
change x ∈ RingHom.ker f'.toRingHom
case inr.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
x : RXm
hx : x ∈ ↑s
⊢ x ∈ Ideal.span ↑s
case inr.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
x : RXm
hx : x ∈ ↑s
⊢ x ∈ RingHom.ker ↑f'
rw [← hs]
no goals
case inr.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
x : RXm
hx : x ∈ ↑s
⊢ x ∈ Ideal.span ↑s
exact Ideal.subset_span hx
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
⊢ x ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
⊢ x ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
have : x ∈ adjoin R (Set.range X : Set RXn) := by
  rw [adjoin_range_X]
  trivial
case refine_1
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
⊢ ∀ (x : RXn),
    x ∈ Set.range MvPolynomial.X → x ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid

case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
⊢ ∀ (r : R), ↑(algebraMap R RXn) r ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid

case refine_3
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
⊢ ∀ (x y : RXn),
    x ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid →
      y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid →
        x + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid

case refine_4
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
⊢ ∀ (x y : RXn),
    x ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid →
      y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid →
        x * y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
⊢ x ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
refine adjoin_induction this ?_ ?_ ?_ ?_
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
⊢ x ∈ ⊤
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
⊢ x ∈ adjoin R (Set.range MvPolynomial.X)
rw [adjoin_range_X]
no goals
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
⊢ x ∈ ⊤
trivial
case refine_1.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
case refine_1
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
⊢ ∀ (x : RXn),
    x ∈ Set.range MvPolynomial.X → x ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
rintro _ ⟨i, rfl⟩
case refine_1.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
i : Fin n
⊢ ↑(MvPolynomial.aeval h) (g i) + (MvPolynomial.X i - ↑(MvPolynomial.aeval h) (g i)) ∈
    Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
case refine_1.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
rw [← sub_add_cancel (X i) (aeval h (g i)), add_comm]
case refine_1.intro.hx
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
i : Fin n
⊢ ↑(MvPolynomial.aeval h) (g i) ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h)

case refine_1.intro.hy
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i - ↑(MvPolynomial.aeval h) (g i) ∈ (Ideal.span s').toAddSubmonoid
case refine_1.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
i : Fin n
⊢ ↑(MvPolynomial.aeval h) (g i) + (MvPolynomial.X i - ↑(MvPolynomial.aeval h) (g i)) ∈
    Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
apply AddSubmonoid.add_mem_sup
no goals
case refine_1.intro.hx
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
i : Fin n
⊢ ↑(MvPolynomial.aeval h) (g i) ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h)
exact Set.mem_range_self _
case refine_1.intro.hy.a
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i - ↑(MvPolynomial.aeval h) (g i) ∈ s'
case refine_1.intro.hy
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i - ↑(MvPolynomial.aeval h) (g i) ∈ (Ideal.span s').toAddSubmonoid
apply Submodule.subset_span
case refine_1.intro.hy.a.a
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i - ↑(MvPolynomial.aeval h) (g i) ∈ Set.range g'
case refine_1.intro.hy.a
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i - ↑(MvPolynomial.aeval h) (g i) ∈ s'
apply Set.mem_union_left
no goals
case refine_1.intro.hy.a.a
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i - ↑(MvPolynomial.aeval h) (g i) ∈ Set.range g'
exact Set.mem_range_self _
case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
r : R
⊢ ↑(algebraMap R RXn) r ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
⊢ ∀ (r : R), ↑(algebraMap R RXn) r ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
intro r
case refine_2.a
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
r : R
⊢ ↑(algebraMap R RXn) r ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h)
case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
r : R
⊢ ↑(algebraMap R RXn) r ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
apply AddSubmonoid.mem_sup_left
no goals
case refine_2.a
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
r : R
⊢ ↑(algebraMap R RXn) r ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h)
exact ⟨C r, aeval_C _ _⟩
case refine_3
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
x✝ y✝ : RXn
h₁ : x✝ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
h₂ : y✝ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ x✝ + y✝ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
case refine_3
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
⊢ ∀ (x y : RXn),
    x ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid →
      y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid →
        x + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
intro _ _ h₁ h₂
no goals
case refine_3
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
x✝ y✝ : RXn
h₁ : x✝ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
h₂ : y✝ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ x✝ + y✝ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
exact add_mem h₁ h₂
case refine_4
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
p₁ p₂ : RXn
h₁ : p₁ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
h₂ : p₂ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ p₁ * p₂ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
case refine_4
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
⊢ ∀ (x y : RXn),
    x ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid →
      y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid →
        x * y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
intro p₁ p₂ h₁ h₂
case refine_4.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
p₂ : RXn
h₂ : p₂ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
x₁ : RXm
y₁ : RXn
hy₁ : y₁ ∈ (Ideal.span s').toAddSubmonoid
h₁ : ↑↑aeval_h x₁ + y₁ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ (↑↑aeval_h x₁ + y₁) * p₂ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
case refine_4
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
p₁ p₂ : RXn
h₁ : p₁ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
h₂ : p₂ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ p₁ * p₂ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
obtain ⟨_, ⟨x₁, rfl⟩, y₁, hy₁, rfl⟩ := AddSubmonoid.mem_sup.mp h₁
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
x₁ : RXm
y₁ : RXn
hy₁ : y₁ ∈ (Ideal.span s').toAddSubmonoid
h₁ : ↑↑aeval_h x₁ + y₁ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
x₂ : RXm
y₂ : RXn
hy₂ : y₂ ∈ (Ideal.span s').toAddSubmonoid
h₂ : ↑↑aeval_h x₂ + y₂ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ (↑↑aeval_h x₁ + y₁) * (↑↑aeval_h x₂ + y₂) ∈
    Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
case refine_4.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
p₂ : RXn
h₂ : p₂ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
x₁ : RXm
y₁ : RXn
hy₁ : y₁ ∈ (Ideal.span s').toAddSubmonoid
h₁ : ↑↑aeval_h x₁ + y₁ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ (↑↑aeval_h x₁ + y₁) * p₂ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
obtain ⟨_, ⟨x₂, rfl⟩, y₂, hy₂, rfl⟩ := AddSubmonoid.mem_sup.mp h₂
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
x₁ : RXm
y₁ : RXn
hy₁ : y₁ ∈ (Ideal.span s').toAddSubmonoid
h₁ : ↑↑aeval_h x₁ + y₁ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
x₂ : RXm
y₂ : RXn
hy₂ : y₂ ∈ (Ideal.span s').toAddSubmonoid
h₂ : ↑↑aeval_h x₂ + y₂ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ ↑↑aeval_h (x₁ * x₂) + (y₁ * ↑↑aeval_h x₂ + (↑↑aeval_h x₁ + y₁) * y₂) ∈
    Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
x₁ : RXm
y₁ : RXn
hy₁ : y₁ ∈ (Ideal.span s').toAddSubmonoid
h₁ : ↑↑aeval_h x₁ + y₁ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
x₂ : RXm
y₂ : RXn
hy₂ : y₂ ∈ (Ideal.span s').toAddSubmonoid
h₂ : ↑↑aeval_h x₂ + y₂ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ (↑↑aeval_h x₁ + y₁) * (↑↑aeval_h x₂ + y₂) ∈
    Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
rw [mul_add, add_mul, add_assoc, ← map_mul]
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hx
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
x₁ : RXm
y₁ : RXn
hy₁ : y₁ ∈ (Ideal.span s').toAddSubmonoid
h₁ : ↑↑aeval_h x₁ + y₁ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
x₂ : RXm
y₂ : RXn
hy₂ : y₂ ∈ (Ideal.span s').toAddSubmonoid
h₂ : ↑↑aeval_h x₂ + y₂ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ ↑↑aeval_h (x₁ * x₂) ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h)

case refine_4.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hy
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
x₁ : RXm
y₁ : RXn
hy₁ : y₁ ∈ (Ideal.span s').toAddSubmonoid
h₁ : ↑↑aeval_h x₁ + y₁ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
x₂ : RXm
y₂ : RXn
hy₂ : y₂ ∈ (Ideal.span s').toAddSubmonoid
h₂ : ↑↑aeval_h x₂ + y₂ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ y₁ * ↑↑aeval_h x₂ + (↑↑aeval_h x₁ + y₁) * y₂ ∈ (Ideal.span s').toAddSubmonoid
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
x₁ : RXm
y₁ : RXn
hy₁ : y₁ ∈ (Ideal.span s').toAddSubmonoid
h₁ : ↑↑aeval_h x₁ + y₁ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
x₂ : RXm
y₂ : RXn
hy₂ : y₂ ∈ (Ideal.span s').toAddSubmonoid
h₂ : ↑↑aeval_h x₂ + y₂ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ ↑↑aeval_h (x₁ * x₂) + (y₁ * ↑↑aeval_h x₂ + (↑↑aeval_h x₁ + y₁) * y₂) ∈
    Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
apply AddSubmonoid.add_mem_sup
no goals
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hx
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
x₁ : RXm
y₁ : RXn
hy₁ : y₁ ∈ (Ideal.span s').toAddSubmonoid
h₁ : ↑↑aeval_h x₁ + y₁ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
x₂ : RXm
y₂ : RXn
hy₂ : y₂ ∈ (Ideal.span s').toAddSubmonoid
h₂ : ↑↑aeval_h x₂ + y₂ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ ↑↑aeval_h (x₁ * x₂) ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h)
exact Set.mem_range_self _
no goals
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.hy
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXn
hx : x ∈ RingHom.ker ↑f
this : x ∈ adjoin R (Set.range MvPolynomial.X)
x₁ : RXm
y₁ : RXn
hy₁ : y₁ ∈ (Ideal.span s').toAddSubmonoid
h₁ : ↑↑aeval_h x₁ + y₁ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
x₂ : RXm
y₂ : RXn
hy₂ : y₂ ∈ (Ideal.span s').toAddSubmonoid
h₂ : ↑↑aeval_h x₂ + y₂ ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
⊢ y₁ * ↑↑aeval_h x₂ + (↑↑aeval_h x₁ + y₁) * y₂ ∈ (Ideal.span s').toAddSubmonoid
exact add_mem (Ideal.mul_mem_right _ _ hy₁) (Ideal.mul_mem_left _ _ hy₂)
case a
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
this✝ : ↑↑aeval_h x + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
hx : ↑f' x = 0
this : Ideal.span ↑s ≤ Ideal.comap aeval_h (Ideal.span s')
⊢ x ∈ Ideal.span ↑s
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
this✝ : ↑↑aeval_h x + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
hx : ↑f' x = 0
this : Ideal.span ↑s ≤ Ideal.comap aeval_h (Ideal.span s')
⊢ ↑↑aeval_h x ∈ Ideal.span s'
apply this
no goals
case a
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ↑f
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ↑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker ↑f'
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), ↑f' (g i) = ↑f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), ↑f (h i) = ↑f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i => MvPolynomial.X i - ↑aeval_h (g i)
hh' : ∀ (x : RXm), ↑f (↑aeval_h x) = ↑f' x
s' : Set RXn := Set.range g' ∪ ↑aeval_h '' ↑s
leI : Ideal.span s' ≤ RingHom.ker ↑f
x : RXm
y : RXn
hy : y ∈ (Ideal.span s').toAddSubmonoid
this✝ : ↑↑aeval_h x + y ∈ Subalgebra.toAddSubmonoid (AlgHom.range aeval_h) ⊔ (Ideal.span s').toAddSubmonoid
hx : ↑f' x = 0
this : Ideal.span ↑s ≤ Ideal.comap aeval_h (Ideal.span s')
⊢ x ∈ Ideal.span ↑s
rwa [hs]