-- Mathlib/RingTheory/FinitePresentation.lean
theorem of_restrict_scalars_finitePresentation [Algebra A B] [IsScalarTower R A B]
    [FinitePresentation.{w₁, w₃} R B] [FiniteType R A] :
    FinitePresentation.{w₂, w₃} A B

Proof state:
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
inst✝¹ : FinitePresentation R B
inst✝ : 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.toRingHom
RX : Type (max 0 w₁) := MvPolynomial (Fin n) R
AX : Type (max 0 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

Tactic:
have := Ideal.subset_span hx

Result:
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
inst✝¹ : FinitePresentation R B
inst✝ : 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.toRingHom
RX : Type (max 0 w₁) := MvPolynomial (Fin n) R
AX : Type (max 0 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

Proof state:
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
inst✝¹ : FinitePresentation R B
inst✝ : 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.toRingHom
RX : Type (max 0 w₁) := MvPolynomial (Fin n) R
AX : Type (max 0 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 ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid

Tactic:
rw [← ht''] at this

Result:
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
inst✝¹ : FinitePresentation R B
inst✝ : 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.toRingHom
RX : Type (max 0 w₁) := MvPolynomial (Fin n) R
AX : Type (max 0 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.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid

Proof state:
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
inst✝¹ : FinitePresentation R B
inst✝ : 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.toRingHom
RX : Type (max 0 w₁) := MvPolynomial (Fin n) R
AX : Type (max 0 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 ∈
    (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid
this : RingHom.ker f.toRingHom ≤ Ideal.comap (MvPolynomial.map (algebraMap R A)) (Ideal.span s₀)
⊢ (MvPolynomial.map (algebraMap R A)) p ∈ Ideal.span s₀

Tactic:
exact this hx

Result:
no goals