-- Mathlib/RingTheory/Presentation.lean
private lemma span_range_relation_eq_ker_baseChange :
    Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i)) =
      RingHom.ker (aeval (R := T) (S₁ := T ⊗[R] S) P.baseChange.val)

Proof state:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S
x : MvPolynomial P.vars T
hx : (aeval P.baseChange.val) x = 0
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial P.vars R ≃ₐ[T] MvPolynomial P.vars T := algebraTensorAlgEquiv R T
⊢ e.symm x ∈ RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S))

Tactic:
rw [RingHom.mem_ker, ← hx]

Result:
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S
x : MvPolynomial P.vars T
hx : (aeval P.baseChange.val) x = 0
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial P.vars R ≃ₐ[T] MvPolynomial P.vars T := algebraTensorAlgEquiv R T
⊢ (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm x) = (aeval P.baseChange.val) x

Proof state:
case h_C
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial P.vars R ≃ₐ[T] MvPolynomial P.vars T := algebraTensorAlgEquiv R T
a : T
⊢ (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S))
      ((algebraMap T (T ⊗[R] MvPolynomial P.vars R)) a) =
    (aeval P.baseChange.val) ((algebraMap T (MvPolynomial P.vars T)) a)

Tactic:
simp only [TensorProduct.algebraMap_apply, id.map_eq_id, RingHom.id_apply,
  TensorProduct.map_tmul, AlgHom.coe_id, id_eq, map_one, algebraMap_eq]

Result:
case h_C
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial P.vars R ≃ₐ[T] MvPolynomial P.vars T := algebraTensorAlgEquiv R T
a : T
⊢ a ⊗ₜ[R] 1 = (aeval P.baseChange.val) (C a)

Proof state:
case a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S
x : MvPolynomial P.vars T
y : P.rels
hy : (fun i => (MvPolynomial.map (algebraMap R T)) (P.relation i)) y = x
Z : TensorProduct.includeRight ((aeval P.val) (P.relation y)) = 0
⊢ (aeval P.baseChange.val) (P.relation y) =
    (eval₂Hom (algebraMap R (T ⊗[R] S)) fun i => TensorProduct.includeRight.toRingHom (P.val i)) (P.relation y)

Tactic:
rfl

Result:
no goals

Proof state:
case a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S
x : MvPolynomial P.vars T
y : P.rels
hy : (fun i => (MvPolynomial.map (algebraMap R T)) (P.relation i)) y = x
Z : TensorProduct.includeRight ((aeval P.val) (P.relation y)) = 0
⊢ (aeval P.baseChange.val) (P.relation y) = TensorProduct.includeRight ((aeval P.val) (P.relation y))

Tactic:
erw [map_aeval, TensorProduct.includeRight.comp_algebraMap]

Result:
case a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S
x : MvPolynomial P.vars T
y : P.rels
hy : (fun i => (MvPolynomial.map (algebraMap R T)) (P.relation i)) y = x
Z : TensorProduct.includeRight ((aeval P.val) (P.relation y)) = 0
⊢ (aeval P.baseChange.val) (P.relation y) =
    (eval₂Hom (algebraMap R (T ⊗[R] S)) fun i => TensorProduct.includeRight.toRingHom (P.val i)) (P.relation y)

Proof state:
case a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S
x : MvPolynomial P.vars T
hx : (aeval P.baseChange.val) x = 0
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial P.vars R ≃ₐ[T] MvPolynomial P.vars T := algebraTensorAlgEquiv R T
H' :
  x ∈
    Ideal.span
      (Set.range
        (⇑((TensorProduct.lift (ofId T (MvPolynomial P.vars T)) (mapAlgHom (ofId R T)) ⋯).comp
              TensorProduct.includeRight.toRingHom) ∘
          P.relation))
⊢ x ∈ Ideal.span (Set.range fun i => (MvPolynomial.map (algebraMap R T)) (P.relation i))

Tactic:
convert H'

Result:
case h.e'_4.h.e'_3.h.e'_3.h
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S
x : MvPolynomial P.vars T
hx : (aeval P.baseChange.val) x = 0
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial P.vars R ≃ₐ[T] MvPolynomial P.vars T := algebraTensorAlgEquiv R T
H' :
  x ∈
    Ideal.span
      (Set.range
        (⇑((TensorProduct.lift (ofId T (MvPolynomial P.vars T)) (mapAlgHom (ofId R T)) ⋯).comp
              TensorProduct.includeRight.toRingHom) ∘
          P.relation))
x✝ : P.rels
⊢ (MvPolynomial.map (algebraMap R T)) (P.relation x✝) =
    (⇑((TensorProduct.lift (ofId T (MvPolynomial P.vars T)) (mapAlgHom (ofId R T)) ⋯).comp
            TensorProduct.includeRight.toRingHom) ∘
        P.relation)
      x✝

Proof state:
case a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S
⊢ (Set.range fun i => (MvPolynomial.map (algebraMap R T)) (P.relation i)) ⊆ ↑(RingHom.ker (aeval P.baseChange.val))

Tactic:
intro x ⟨y, hy⟩

Result:
case a
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S
x : MvPolynomial P.vars T
y : P.rels
hy : (fun i => (MvPolynomial.map (algebraMap R T)) (P.relation i)) y = x
⊢ x ∈ ↑(RingHom.ker (aeval P.baseChange.val))