-- 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
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

Tactic:
induction x using MvPolynomial.induction_on with
| h_C a =>
  simp only [Generators.algebraMap_apply, algHom_C, TensorProduct.algebraMap_apply,
    id.map_eq_id, RingHom.id_apply, e]
  rw [← MvPolynomial.algebraMap_eq, AlgEquiv.commutes]
  simp only [TensorProduct.algebraMap_apply, id.map_eq_id, RingHom.id_apply,
    TensorProduct.map_tmul, AlgHom.coe_id, id_eq, map_one, algebraMap_eq]
  erw [aeval_C]
  simp
| h_add p q hp hq => simp only [map_add, hp, hq]
| h_X p i hp =>
  simp only [map_mul, algebraTensorAlgEquiv_symm_X, hp, TensorProduct.map_tmul, map_one,
    IsScalarTower.coe_toAlgHom', Generators.algebraMap_apply, aeval_X, e]
  congr
  erw [aeval_X]
  rw [Generators.baseChange_val]

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
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' : e.symm x ∈ Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
⊢ x ∈ Ideal.span (Set.range fun i => (MvPolynomial.map (algebraMap R T)) (P.relation i))

Tactic:
replace H' : e.symm x ∈ Ideal.map TensorProduct.includeRight P.ker := H'

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
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' : e.symm x ∈ Ideal.map TensorProduct.includeRight P.ker
⊢ x ∈ Ideal.span (Set.range fun i => (MvPolynomial.map (algebraMap R T)) (P.relation i))

Proof state:
case h_add
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
p q : MvPolynomial P.vars T
hp : (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm p) = (aeval P.baseChange.val) p
hq : (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm q) = (aeval P.baseChange.val) q
⊢ (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm (p + q)) =
    (aeval P.baseChange.val) (p + q)

Tactic:
simp only [map_add, hp, hq]

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
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' : e.symm x ∈ Ideal.map TensorProduct.includeRight P.ker
⊢ x ∈ Ideal.span (Set.range fun i => (MvPolynomial.map (algebraMap R T)) (P.relation i))

Tactic:
erw [← P.span_range_relation_eq_ker, ← Ideal.mem_comap, Ideal.comap_symm,
  Ideal.map_map, Ideal.map_span, ← Set.range_comp] at H'

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
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))

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 : x ∈ RingHom.ker (aeval P.baseChange.val)
⊢ x ∈ Ideal.span (Set.range fun i => (MvPolynomial.map (algebraMap R T)) (P.relation i))

Tactic:
rw [RingHom.mem_ker] at hx

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
hx : (aeval P.baseChange.val) x = 0
⊢ x ∈ Ideal.span (Set.range fun i => (MvPolynomial.map (algebraMap R T)) (P.relation i))

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
⊢ x ∈ ↑(RingHom.ker (aeval P.baseChange.val))

Tactic:
have Z := aeval_val_relation P y

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 : (aeval P.val) (P.relation y) = 0
⊢ x ∈ ↑(RingHom.ker (aeval P.baseChange.val))