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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
⊢ FinitePresentation A B
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRB : FinitePresentation R B
hRA : FiniteType R A
⊢ FinitePresentation A B
obtain ⟨n, f, hf, s, hs⟩ := hRB
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
⊢ FinitePresentation A B
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
⊢ FinitePresentation A B
letI RX := 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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
⊢ FinitePresentation A B
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
⊢ FinitePresentation A B
letI AX := MvPolynomial (Fin n) A
case intro.intro.intro.intro.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
⊢ Surjective ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X))

case intro.intro.intro.intro.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
⊢ Ideal.FG (RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)))
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
⊢ FinitePresentation A B
refine' ⟨n, MvPolynomial.aeval (f ∘ X), _, _⟩
case intro.intro.intro.intro.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
⊢ ∀ (x : B), x ∈ adjoin A ↑⊤
case intro.intro.intro.intro.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
⊢ Surjective ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
rw [← Algebra.range_top_iff_surjective, ← Algebra.adjoin_range_eq_range_aeval,
  Set.range_comp f MvPolynomial.X, eq_top_iff, ← @adjoin_adjoin_of_tower R A B,
  adjoin_image, adjoin_range_X, Algebra.map_top, (Algebra.range_top_iff_surjective _).mpr hf]
no goals
case intro.intro.intro.intro.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
⊢ ∀ (x : B), x ∈ adjoin A ↑⊤
exact fun {x} => subset_adjoin ⟨⟩
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
⊢ Ideal.FG (RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)))
case intro.intro.intro.intro.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
⊢ Ideal.FG (RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)))
obtain ⟨t, ht⟩ := hRA.out
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
this : ∀ (i : { x // x ∈ t }), ∃ a, ↑f a = ↑(algebraMap A B) ↑i
⊢ Ideal.FG (RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)))
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
⊢ Ideal.FG (RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)))
have := fun i : t => hf (algebraMap A B i)
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
⊢ Ideal.FG (RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)))
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
this : ∀ (i : { x // x ∈ t }), ∃ a, ↑f a = ↑(algebraMap A B) ↑i
⊢ Ideal.FG (RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)))
choose t' ht' using this
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
⊢ Ideal.FG (RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)))
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
⊢ Ideal.FG (RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)))
have ht'' : Algebra.adjoin R (algebraMap A AX '' t ∪ Set.range (X : _ → AX)) = ⊤ := by
  rw [adjoin_union_eq_adjoin_adjoin, ← Subalgebra.restrictScalars_top R (A := AX)
    (S := { x // x ∈ adjoin R ((algebraMap A AX) '' t) })]
  refine congrArg (Subalgebra.restrictScalars R) ?_
  congr 1
  rw [adjoin_algebraMap, ht]
  apply Subalgebra.restrictScalars_injective R
  rw [← adjoin_restrictScalars, adjoin_range_X, Subalgebra.restrictScalars_top,
    Subalgebra.restrictScalars_top]
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
⊢ Ideal.FG (RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)))
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
⊢ Ideal.FG (RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)))
letI g : t → AX := fun x => MvPolynomial.C (x : A) - map (algebraMap R A) (t' x)
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
⊢ Ideal.span ↑(Finset.image (↑(MvPolynomial.map (algebraMap R A))) s ∪ Finset.image g (Finset.attach t)) =
    RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
⊢ Ideal.FG (RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)))
refine' ⟨s.image (map (algebraMap R A)) ∪ t.attach.image g, _⟩
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
⊢ Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) =
    RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
⊢ Ideal.span ↑(Finset.image (↑(MvPolynomial.map (algebraMap R A))) s ∪ Finset.image g (Finset.attach t)) =
    RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
rw [Finset.coe_union, Finset.coe_image, Finset.coe_image, Finset.attach_eq_univ,
  Finset.coe_univ, Set.image_univ]
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
⊢ Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) =
    RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
⊢ Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) =
    RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
let s₀ := (MvPolynomial.map (algebraMap R A)) '' s ∪ Set.range g
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
⊢ Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) =
    RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
⊢ Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) =
    RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
let I := RingHom.ker (MvPolynomial.aeval (R := A) (f ∘ MvPolynomial.X))
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
⊢ Ideal.span s₀ = I
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
⊢ Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) =
    RingHom.ker ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
change Ideal.span s₀ = I
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
⊢ RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) ≤
    Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g)
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
⊢ Ideal.span s₀ = I
apply leI.antisymm
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : x ∈ RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
⊢ x ∈ Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g)
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
⊢ RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) ≤
    Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g)
intro x hx
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
⊢ x ∈ Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g)
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : x ∈ RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
⊢ x ∈ Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g)
rw [RingHom.mem_ker] at hx
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
⊢ x ∈ Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g)
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
⊢ x ∈ Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g)
let s₀ := (MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
⊢ x ∈ Ideal.span s₀
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
⊢ x ∈ Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g)
change x ∈ Ideal.span s₀
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) (↑(MvPolynomial.map (algebraMap R A)) p + q) = 0
this :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ ↑(MvPolynomial.map (algebraMap R A)) p + q ∈ Ideal.span s₀
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this :
  x ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ x ∈ Ideal.span s₀
obtain ⟨_, ⟨p, rfl⟩, q, hq, rfl⟩ := AddSubmonoid.mem_sup.mp this
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx : ↑f p = 0
this :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ ↑(MvPolynomial.map (algebraMap R A)) p + q ∈ Ideal.span s₀
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) (↑(MvPolynomial.map (algebraMap R A)) p + q) = 0
this :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ ↑(MvPolynomial.map (algebraMap R A)) p + q ∈ Ideal.span s₀
rw [map_add, aeval_map_algebraMap, ← aeval_unique, show MvPolynomial.aeval (f ∘ X) q = 0
  from leI hq, add_zero] at hx
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx : ↑f p = 0
this :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ Ideal.span ↑s ≤ Ideal.comap (MvPolynomial.map (algebraMap R A)) (Ideal.span s₀)
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx : ↑f p = 0
this :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ ↑(MvPolynomial.map (algebraMap R A)) p + q ∈ Ideal.span s₀
suffices Ideal.span (s : Set RX) ≤ (Ideal.span s₀).comap (MvPolynomial.map <| algebraMap R A) by
  refine' add_mem _ hq
  rw [hs] at this
  exact this hx
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx : ↑f p = 0
this :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ ↑s ⊆ ↑(Ideal.comap (MvPolynomial.map (algebraMap R A)) (Ideal.span s₀))
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx : ↑f p = 0
this :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ Ideal.span ↑s ≤ Ideal.comap (MvPolynomial.map (algebraMap R A)) (Ideal.span s₀)
rw [Ideal.span_le]
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx✝ : ↑f p = 0
this :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
x : MvPolynomial (Fin n) R
hx : x ∈ ↑s
⊢ x ∈ ↑(Ideal.comap (MvPolynomial.map (algebraMap R A)) (Ideal.span s₀))
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx : ↑f p = 0
this :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ ↑s ⊆ ↑(Ideal.comap (MvPolynomial.map (algebraMap R A)) (Ideal.span s₀))
intro x hx
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx✝ : ↑f p = 0
this :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
x : MvPolynomial (Fin n) R
hx : x ∈ ↑s
⊢ ↑(MvPolynomial.map (algebraMap R A)) x ∈ s₀
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx✝ : ↑f p = 0
this :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
x : MvPolynomial (Fin n) R
hx : x ∈ ↑s
⊢ x ∈ ↑(Ideal.comap (MvPolynomial.map (algebraMap R A)) (Ideal.span s₀))
apply Ideal.subset_span
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx✝ : ↑f p = 0
this :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
x : MvPolynomial (Fin n) R
hx : x ∈ ↑s
⊢ ↑(MvPolynomial.map (algebraMap R A)) x ∈ ↑(MvPolynomial.map (algebraMap R A)) '' ↑s
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx✝ : ↑f p = 0
this :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
x : MvPolynomial (Fin n) R
hx : x ∈ ↑s
⊢ ↑(MvPolynomial.map (algebraMap R A)) x ∈ s₀
apply Set.mem_union_left
no goals
case intro.intro.intro.intro.refine'_2.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx✝ : ↑f p = 0
this :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
x : MvPolynomial (Fin n) R
hx : x ∈ ↑s
⊢ ↑(MvPolynomial.map (algebraMap R A)) x ∈ ↑(MvPolynomial.map (algebraMap R A)) '' ↑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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
⊢ Subalgebra.restrictScalars R (adjoin { x // x ∈ adjoin R (↑(algebraMap A AX) '' ↑t) } (Set.range MvPolynomial.X)) =
    Subalgebra.restrictScalars R ⊤
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
⊢ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
rw [adjoin_union_eq_adjoin_adjoin, ← Subalgebra.restrictScalars_top R (A := AX)
  (S := { x // x ∈ adjoin R ((algebraMap A AX) '' t) })]
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
⊢ adjoin { x // x ∈ adjoin R (↑(algebraMap A AX) '' ↑t) } (Set.range MvPolynomial.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
⊢ Subalgebra.restrictScalars R (adjoin { x // x ∈ adjoin R (↑(algebraMap A AX) '' ↑t) } (Set.range MvPolynomial.X)) =
    Subalgebra.restrictScalars R ⊤
refine congrArg (Subalgebra.restrictScalars R) ?_
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
⊢ adjoin { x // x ∈ adjoin R (↑(algebraMap A AX) '' ↑t) } (Set.range MvPolynomial.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
⊢ adjoin { x // x ∈ adjoin R (↑(algebraMap A AX) '' ↑t) } (Set.range MvPolynomial.X) = ⊤
congr 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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
⊢ adjoin { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤ } (Set.range MvPolynomial.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
⊢ adjoin { x // x ∈ adjoin R (↑(algebraMap A AX) '' ↑t) } (Set.range MvPolynomial.X) = ⊤
rw [adjoin_algebraMap, ht]
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
⊢ Subalgebra.restrictScalars R
      (adjoin { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤ } (Set.range MvPolynomial.X)) =
    Subalgebra.restrictScalars R ⊤
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
⊢ adjoin { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤ } (Set.range MvPolynomial.X) = ⊤
apply Subalgebra.restrictScalars_injective R
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
⊢ Subalgebra.restrictScalars R
      (adjoin { x // x ∈ Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤ } (Set.range MvPolynomial.X)) =
    Subalgebra.restrictScalars R ⊤
rw [← adjoin_restrictScalars, adjoin_range_X, Subalgebra.restrictScalars_top,
  Subalgebra.restrictScalars_top]
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
⊢ ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g ⊆ ↑(RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
⊢ Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
rw [Ideal.span_le]
case inl.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) R
hx : x ∈ ↑s
⊢ ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) (↑(MvPolynomial.map (algebraMap R A)) x) = 0

case inr.intro.mk
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : A
hx : x ∈ t
⊢ ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) (g { val := x, property := hx }) = 0
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
⊢ ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g ⊆ ↑(RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X)))
rintro _ (⟨x, hx, rfl⟩ | ⟨⟨x, hx⟩, rfl⟩) <;>
erw [RingHom.mem_ker]
case inl.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) R
hx : x ∈ ↑s
⊢ ↑f x = 0
case inl.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) R
hx : x ∈ ↑s
⊢ ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) (↑(MvPolynomial.map (algebraMap R A)) x) = 0
rw [MvPolynomial.aeval_map_algebraMap (R := R) (A := A), ← aeval_unique]
case inl.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) R
hx : x ∈ ↑s
this : x ∈ ↑(Ideal.span ↑s)
⊢ ↑f x = 0
case inl.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) R
hx : x ∈ ↑s
⊢ ↑f x = 0
have := Ideal.subset_span hx
no goals
case inl.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) R
hx : x ∈ ↑s
this : x ∈ ↑(Ideal.span ↑s)
⊢ ↑f x = 0
rwa [hs] at this
no goals
case inr.intro.mk
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : A
hx : x ∈ t
⊢ ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) (g { val := x, property := hx }) = 0
rw [map_sub, MvPolynomial.aeval_map_algebraMap, ← aeval_unique,
  MvPolynomial.aeval_C, ht', Subtype.coe_mk, sub_self]
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ ⊤
⊢ x ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
⊢ x ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
have : x ∈ (⊤ : Subalgebra R AX) := trivial
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
⊢ x ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ ⊤
⊢ x ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
rw [← ht''] at this
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
⊢ ∀ (x : MvPolynomial (Fin n) A),
    x ∈ ↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X →
      x ∈
        Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
          (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
⊢ ∀ (r : R),
    ↑(algebraMap R (MvPolynomial (Fin n) A)) r ∈
      Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
        (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
⊢ ∀ (x y : MvPolynomial (Fin n) A),
    x ∈
        Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
          (Ideal.span s₀).toAddSubmonoid →
      y ∈
          Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
            (Ideal.span s₀).toAddSubmonoid →
        x + y ∈
          Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
            (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
⊢ ∀ (x y : MvPolynomial (Fin n) A),
    x ∈
        Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
          (Ideal.span s₀).toAddSubmonoid →
      y ∈
          Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
            (Ideal.span s₀).toAddSubmonoid →
        x * y ∈
          Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
            (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
⊢ x ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
refine adjoin_induction this ?_ ?_ ?_ ?_
case refine_1.inl.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x✝ : MvPolynomial (Fin n) A
hx✝ : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x✝ = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x✝ ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x : A
hx : x ∈ ↑t
⊢ ↑(algebraMap A AX) x ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid

case refine_1.inr.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
⊢ ∀ (x : MvPolynomial (Fin n) A),
    x ∈ ↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X →
      x ∈
        Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
          (Ideal.span s₀).toAddSubmonoid
rintro _ (⟨x, hx, rfl⟩ | ⟨i, rfl⟩)
case refine_1.inl.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x✝ : MvPolynomial (Fin n) A
hx✝ : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x✝ = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x✝ ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x : A
hx : x ∈ ↑t
⊢ ↑(MvPolynomial.map (algebraMap R A)) (t' { val := x, property := hx }) +
      (↑MvPolynomial.C x - ↑(MvPolynomial.map (algebraMap R A)) (t' { val := x, property := hx })) ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
case refine_1.inl.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x✝ : MvPolynomial (Fin n) A
hx✝ : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x✝ = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x✝ ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x : A
hx : x ∈ ↑t
⊢ ↑(algebraMap A AX) x ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
rw [algebraMap_eq, ← sub_add_cancel (MvPolynomial.C x)
  (map (algebraMap R A) (t' ⟨x, hx⟩)), add_comm]
case refine_1.inl.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x✝ : MvPolynomial (Fin n) A
hx✝ : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x✝ = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x✝ ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x : A
hx : x ∈ ↑t
⊢ ↑(MvPolynomial.map (algebraMap R A)) (t' { val := x, property := hx }) ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring

case refine_1.inl.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x✝ : MvPolynomial (Fin n) A
hx✝ : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x✝ = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x✝ ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x : A
hx : x ∈ ↑t
⊢ ↑MvPolynomial.C x - ↑(MvPolynomial.map (algebraMap R A)) (t' { val := x, property := hx }) ∈
    (Ideal.span s₀).toAddSubmonoid
case refine_1.inl.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x✝ : MvPolynomial (Fin n) A
hx✝ : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x✝ = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x✝ ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x : A
hx : x ∈ ↑t
⊢ ↑(MvPolynomial.map (algebraMap R A)) (t' { val := x, property := hx }) +
      (↑MvPolynomial.C x - ↑(MvPolynomial.map (algebraMap R A)) (t' { val := x, property := hx })) ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
apply AddSubmonoid.add_mem_sup
no goals
case refine_1.inl.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x✝ : MvPolynomial (Fin n) A
hx✝ : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x✝ = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x✝ ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x : A
hx : x ∈ ↑t
⊢ ↑(MvPolynomial.map (algebraMap R A)) (t' { val := x, property := hx }) ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring
exact Set.mem_range_self _
case refine_1.inl.intro.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x✝ : MvPolynomial (Fin n) A
hx✝ : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x✝ = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x✝ ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x : A
hx : x ∈ ↑t
⊢ ↑MvPolynomial.C x - ↑(MvPolynomial.map (algebraMap R A)) (t' { val := x, property := hx }) ∈ s₀
case refine_1.inl.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x✝ : MvPolynomial (Fin n) A
hx✝ : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x✝ = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x✝ ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x : A
hx : x ∈ ↑t
⊢ ↑MvPolynomial.C x - ↑(MvPolynomial.map (algebraMap R A)) (t' { val := x, property := hx }) ∈
    (Ideal.span s₀).toAddSubmonoid
apply Ideal.subset_span
case refine_1.inl.intro.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x✝ : MvPolynomial (Fin n) A
hx✝ : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x✝ = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x✝ ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x : A
hx : x ∈ ↑t
⊢ ↑MvPolynomial.C x - ↑(MvPolynomial.map (algebraMap R A)) (t' { val := x, property := hx }) ∈ Set.range g
case refine_1.inl.intro.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x✝ : MvPolynomial (Fin n) A
hx✝ : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x✝ = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x✝ ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x : A
hx : x ∈ ↑t
⊢ ↑MvPolynomial.C x - ↑(MvPolynomial.map (algebraMap R A)) (t' { val := x, property := hx }) ∈ s₀
apply Set.mem_union_right
no goals
case refine_1.inl.intro.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x✝ : MvPolynomial (Fin n) A
hx✝ : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x✝ = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x✝ ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x : A
hx : x ∈ ↑t
⊢ ↑MvPolynomial.C x - ↑(MvPolynomial.map (algebraMap R A)) (t' { val := x, property := hx }) ∈ Set.range g
exact Set.mem_range_self _
case refine_1.inr.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i ∈ Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring
case refine_1.inr.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
apply AddSubmonoid.mem_sup_left
no goals
case refine_1.inr.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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i ∈ Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring
exact ⟨X i, map_X _ _⟩
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
r : R
⊢ ↑(algebraMap R (MvPolynomial (Fin n) A)) r ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
⊢ ∀ (r : R),
    ↑(algebraMap R (MvPolynomial (Fin n) A)) r ∈
      Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
        (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
r : R
⊢ ↑(algebraMap R (MvPolynomial (Fin n) A)) r ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
r : R
⊢ ↑(algebraMap R (MvPolynomial (Fin n) A)) r ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
r : R
⊢ ↑(algebraMap R (MvPolynomial (Fin n) A)) r ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring
exact ⟨C r, map_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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x✝ y✝ : MvPolynomial (Fin n) A
h₁ :
  x✝ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
h₂ :
  y✝ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ x✝ + y✝ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
⊢ ∀ (x y : MvPolynomial (Fin n) A),
    x ∈
        Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
          (Ideal.span s₀).toAddSubmonoid →
      y ∈
          Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
            (Ideal.span s₀).toAddSubmonoid →
        x + y ∈
          Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
            (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x✝ y✝ : MvPolynomial (Fin n) A
h₁ :
  x✝ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
h₂ :
  y✝ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ x✝ + y✝ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x₁ x₂ : MvPolynomial (Fin n) A
h₁ :
  x₁ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
h₂ :
  x₂ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ x₁ * x₂ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
⊢ ∀ (x y : MvPolynomial (Fin n) A),
    x ∈
        Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
          (Ideal.span s₀).toAddSubmonoid →
      y ∈
          Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
            (Ideal.span s₀).toAddSubmonoid →
        x * y ∈
          Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
            (Ideal.span s₀).toAddSubmonoid
intro x₁ x₂ 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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x₂ : MvPolynomial (Fin n) A
h₂ :
  x₂ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
p₁ : MvPolynomial (Fin n) R
q₁ : MvPolynomial (Fin n) A
hq₁ : q₁ ∈ (Ideal.span s₀).toAddSubmonoid
h₁ :
  ↑(MvPolynomial.map (algebraMap R A)) p₁ + q₁ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ (↑(MvPolynomial.map (algebraMap R A)) p₁ + q₁) * x₂ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x₁ x₂ : MvPolynomial (Fin n) A
h₁ :
  x₁ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
h₂ :
  x₂ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ x₁ * x₂ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
obtain ⟨_, ⟨p₁, rfl⟩, q₁, hq₁, 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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
p₁ : MvPolynomial (Fin n) R
q₁ : MvPolynomial (Fin n) A
hq₁ : q₁ ∈ (Ideal.span s₀).toAddSubmonoid
h₁ :
  ↑(MvPolynomial.map (algebraMap R A)) p₁ + q₁ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
p₂ : MvPolynomial (Fin n) R
q₂ : MvPolynomial (Fin n) A
hq₂ : q₂ ∈ (Ideal.span s₀).toAddSubmonoid
h₂ :
  ↑(MvPolynomial.map (algebraMap R A)) p₂ + q₂ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ (↑(MvPolynomial.map (algebraMap R A)) p₁ + q₁) * (↑(MvPolynomial.map (algebraMap R A)) p₂ + q₂) ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x₂ : MvPolynomial (Fin n) A
h₂ :
  x₂ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
p₁ : MvPolynomial (Fin n) R
q₁ : MvPolynomial (Fin n) A
hq₁ : q₁ ∈ (Ideal.span s₀).toAddSubmonoid
h₁ :
  ↑(MvPolynomial.map (algebraMap R A)) p₁ + q₁ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ (↑(MvPolynomial.map (algebraMap R A)) p₁ + q₁) * x₂ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
obtain ⟨_, ⟨p₂, rfl⟩, q₂, hq₂, 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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
p₁ : MvPolynomial (Fin n) R
q₁ : MvPolynomial (Fin n) A
hq₁ : q₁ ∈ (Ideal.span s₀).toAddSubmonoid
h₁ :
  ↑(MvPolynomial.map (algebraMap R A)) p₁ + q₁ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
p₂ : MvPolynomial (Fin n) R
q₂ : MvPolynomial (Fin n) A
hq₂ : q₂ ∈ (Ideal.span s₀).toAddSubmonoid
h₂ :
  ↑(MvPolynomial.map (algebraMap R A)) p₂ + q₂ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ ↑(MvPolynomial.map (algebraMap R A)) (p₁ * p₂) +
      (↑(MvPolynomial.map (algebraMap R A)) p₁ * q₂ + q₁ * (↑(MvPolynomial.map (algebraMap R A)) p₂ + q₂)) ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
p₁ : MvPolynomial (Fin n) R
q₁ : MvPolynomial (Fin n) A
hq₁ : q₁ ∈ (Ideal.span s₀).toAddSubmonoid
h₁ :
  ↑(MvPolynomial.map (algebraMap R A)) p₁ + q₁ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
p₂ : MvPolynomial (Fin n) R
q₂ : MvPolynomial (Fin n) A
hq₂ : q₂ ∈ (Ideal.span s₀).toAddSubmonoid
h₂ :
  ↑(MvPolynomial.map (algebraMap R A)) p₂ + q₂ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ (↑(MvPolynomial.map (algebraMap R A)) p₁ + q₁) * (↑(MvPolynomial.map (algebraMap R A)) p₂ + q₂) ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
rw [add_mul, mul_add, 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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
p₁ : MvPolynomial (Fin n) R
q₁ : MvPolynomial (Fin n) A
hq₁ : q₁ ∈ (Ideal.span s₀).toAddSubmonoid
h₁ :
  ↑(MvPolynomial.map (algebraMap R A)) p₁ + q₁ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
p₂ : MvPolynomial (Fin n) R
q₂ : MvPolynomial (Fin n) A
hq₂ : q₂ ∈ (Ideal.span s₀).toAddSubmonoid
h₂ :
  ↑(MvPolynomial.map (algebraMap R A)) p₂ + q₂ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ ↑(MvPolynomial.map (algebraMap R A)) (p₁ * p₂) ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring

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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
p₁ : MvPolynomial (Fin n) R
q₁ : MvPolynomial (Fin n) A
hq₁ : q₁ ∈ (Ideal.span s₀).toAddSubmonoid
h₁ :
  ↑(MvPolynomial.map (algebraMap R A)) p₁ + q₁ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
p₂ : MvPolynomial (Fin n) R
q₂ : MvPolynomial (Fin n) A
hq₂ : q₂ ∈ (Ideal.span s₀).toAddSubmonoid
h₂ :
  ↑(MvPolynomial.map (algebraMap R A)) p₂ + q₂ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ ↑(MvPolynomial.map (algebraMap R A)) p₁ * q₂ + q₁ * (↑(MvPolynomial.map (algebraMap R A)) p₂ + q₂) ∈
    (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
p₁ : MvPolynomial (Fin n) R
q₁ : MvPolynomial (Fin n) A
hq₁ : q₁ ∈ (Ideal.span s₀).toAddSubmonoid
h₁ :
  ↑(MvPolynomial.map (algebraMap R A)) p₁ + q₁ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
p₂ : MvPolynomial (Fin n) R
q₂ : MvPolynomial (Fin n) A
hq₂ : q₂ ∈ (Ideal.span s₀).toAddSubmonoid
h₂ :
  ↑(MvPolynomial.map (algebraMap R A)) p₂ + q₂ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ ↑(MvPolynomial.map (algebraMap R A)) (p₁ * p₂) +
      (↑(MvPolynomial.map (algebraMap R A)) p₁ * q₂ + q₁ * (↑(MvPolynomial.map (algebraMap R A)) p₂ + q₂)) ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
p₁ : MvPolynomial (Fin n) R
q₁ : MvPolynomial (Fin n) A
hq₁ : q₁ ∈ (Ideal.span s₀).toAddSubmonoid
h₁ :
  ↑(MvPolynomial.map (algebraMap R A)) p₁ + q₁ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
p₂ : MvPolynomial (Fin n) R
q₂ : MvPolynomial (Fin n) A
hq₂ : q₂ ∈ (Ideal.span s₀).toAddSubmonoid
h₂ :
  ↑(MvPolynomial.map (algebraMap R A)) p₂ + q₂ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ ↑(MvPolynomial.map (algebraMap R A)) (p₁ * p₂) ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : ↑(MvPolynomial.aeval (↑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
p₁ : MvPolynomial (Fin n) R
q₁ : MvPolynomial (Fin n) A
hq₁ : q₁ ∈ (Ideal.span s₀).toAddSubmonoid
h₁ :
  ↑(MvPolynomial.map (algebraMap R A)) p₁ + q₁ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
p₂ : MvPolynomial (Fin n) R
q₂ : MvPolynomial (Fin n) A
hq₂ : q₂ ∈ (Ideal.span s₀).toAddSubmonoid
h₂ :
  ↑(MvPolynomial.map (algebraMap R A)) p₂ + q₂ ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
⊢ ↑(MvPolynomial.map (algebraMap R A)) p₁ * q₂ + q₁ * (↑(MvPolynomial.map (algebraMap R A)) p₂ + q₂) ∈
    (Ideal.span s₀).toAddSubmonoid
refine' add_mem (Ideal.mul_mem_left _ _ hq₂) (Ideal.mul_mem_right _ _ hq₁)
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx : ↑f p = 0
this✝ :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
this : Ideal.span ↑s ≤ Ideal.comap (MvPolynomial.map (algebraMap R A)) (Ideal.span s₀)
⊢ ↑(MvPolynomial.map (algebraMap R A)) p ∈ 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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx : ↑f p = 0
this✝ :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
this : Ideal.span ↑s ≤ Ideal.comap (MvPolynomial.map (algebraMap R A)) (Ideal.span s₀)
⊢ ↑(MvPolynomial.map (algebraMap R A)) p + q ∈ Ideal.span s₀
refine' add_mem _ hq
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx : ↑f p = 0
this✝ :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
this : RingHom.ker ↑f ≤ Ideal.comap (MvPolynomial.map (algebraMap R A)) (Ideal.span s₀)
⊢ ↑(MvPolynomial.map (algebraMap R A)) p ∈ 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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx : ↑f p = 0
this✝ :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
this : Ideal.span ↑s ≤ Ideal.comap (MvPolynomial.map (algebraMap R A)) (Ideal.span s₀)
⊢ ↑(MvPolynomial.map (algebraMap R A)) p ∈ Ideal.span s₀
rw [hs] at this
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
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hRA : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ↑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker ↑f
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : { x // x ∈ t } → MvPolynomial (Fin n) R
ht' : ∀ (i : { x // x ∈ t }), ↑f (t' i) = ↑(algebraMap A B) ↑i
ht'' : adjoin R (↑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : { x // x ∈ t } → AX := fun x => ↑MvPolynomial.C ↑x - ↑(MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
leI :
  Ideal.span (↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (↑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ↑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx : ↑f p = 0
this✝ :
  ↑(MvPolynomial.map (algebraMap R A)) p + q ∈
    Subsemiring.toAddSubmonoid (RingHom.range (MvPolynomial.map (algebraMap R A))).toSubsemiring ⊔
      (Ideal.span s₀).toAddSubmonoid
this : RingHom.ker ↑f ≤ Ideal.comap (MvPolynomial.map (algebraMap R A)) (Ideal.span s₀)
⊢ ↑(MvPolynomial.map (algebraMap R A)) p ∈ Ideal.span s₀
exact this hx