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

Tactic:
apply_fun TensorProduct.includeRight (R := R) (A := T) at Z

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

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

Tactic:
let e := MvPolynomial.algebraTensorAlgEquiv (R := R) (σ := P.vars) (A := T)

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

Tactic:
have H := Algebra.TensorProduct.lTensor_ker (A := T) (IsScalarTower.toAlgHom R P.Ring S)
  P.algebraMap_surjective

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

Tactic:
have H' : e.symm x ∈ RingHom.ker (TensorProduct.map (AlgHom.id R T)
    (IsScalarTower.toAlgHom R P.Ring S)) := by
  rw [RingHom.mem_ker, ← hx]
  clear hx
  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:
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 ∈ RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S))
⊢ 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
Z : TensorProduct.includeRight ((aeval P.val) (P.relation y)) = TensorProduct.includeRight 0
⊢ x ∈ ↑(RingHom.ker (aeval P.baseChange.val))

Tactic:
rw [map_zero] at Z

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

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) ((MvPolynomial.map (algebraMap R T)) (P.relation y)) = 1 ⊗ₜ[R] (aeval P.val) (P.relation y)

Tactic:
erw [aeval_map_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) = 1 ⊗ₜ[R] (aeval P.val) (P.relation y)