-- 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 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
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)
p₁ : MvPolynomial (Fin n) R
q₁ : MvPolynomial (Fin n) A
hq₁ : q₁ ∈ (Ideal.span s₀).toAddSubmonoid
hx✝ : (MvPolynomial.map (algebraMap R A)) p₁ + q₁ ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
h₁ :
  (MvPolynomial.map (algebraMap R A)) p₁ + q₁ ∈
    (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid
p₂ : MvPolynomial (Fin n) R
q₂ : MvPolynomial (Fin n) A
hq₂ : q₂ ∈ (Ideal.span s₀).toAddSubmonoid
hy✝ : (MvPolynomial.map (algebraMap R A)) p₂ + q₂ ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
h₂ :
  (MvPolynomial.map (algebraMap R A)) p₂ + q₂ ∈
    (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid
⊢ (MvPolynomial.map (algebraMap R A)) p₁ * q₂ + q₁ * ((MvPolynomial.map (algebraMap R A)) p₂ + q₂) ∈
    (Ideal.span s₀).toAddSubmonoid

Tactic:
refine add_mem (Ideal.mul_mem_left _ _ hq₂) (Ideal.mul_mem_right _ _ hq₁)

Result:
no goals

Proof state:
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
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
x : MvPolynomial (Fin n) R
hx : x ∈ ↑s
⊢ (MvPolynomial.map (algebraMap R A)) x ∈ s₀

Tactic:
apply Set.mem_union_left

Result:
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
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
x : MvPolynomial (Fin n) R
hx : x ∈ ↑s
⊢ (MvPolynomial.map (algebraMap R A)) x ∈ ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s