-- 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 h_X
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 : MvPolynomial P.vars T
i : P.vars
hp : (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm p) = (aeval P.baseChange.val) p
⊢ (aeval P.baseChange.val) p * 1 ⊗ₜ[R] P.val i = (aeval P.baseChange.val) p * (aeval P.baseChange.val) (X i)

Tactic:
congr

Result:
case h_X.e_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
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 : MvPolynomial P.vars T
i : P.vars
hp : (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm p) = (aeval P.baseChange.val) p
⊢ 1 ⊗ₜ[R] P.val i = (aeval P.baseChange.val) (X 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)) = 0
⊢ (aeval P.baseChange.val) (P.relation y) = 1 ⊗ₜ[R] (aeval P.val) (P.relation y)

Tactic:
show _ = TensorProduct.includeRight _

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) = TensorProduct.includeRight ((aeval P.val) (P.relation y))

Proof state:
case h_X.e_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
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 : MvPolynomial P.vars T
i : P.vars
hp : (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm p) = (aeval P.baseChange.val) p
⊢ 1 ⊗ₜ[R] P.val i = (aeval P.baseChange.val) (X i)

Tactic:
erw [aeval_X]

Result:
case h_X.e_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
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 : MvPolynomial P.vars T
i : P.vars
hp : (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm p) = (aeval P.baseChange.val) p
⊢ 1 ⊗ₜ[R] P.val i = P.baseChange.val i

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)) ((algebraTensorAlgEquiv R T).symm (C a)) =
    (aeval P.baseChange.val) (C a)

Tactic:
rw [← MvPolynomial.algebraMap_eq, AlgEquiv.commutes]

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

Proof state:
case h_X.e_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
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 : MvPolynomial P.vars T
i : P.vars
hp : (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm p) = (aeval P.baseChange.val) p
⊢ 1 ⊗ₜ[R] P.val i = P.baseChange.val i

Tactic:
rw [Generators.baseChange_val]

Result:
no goals

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

Tactic:
simp only [map_mul, algebraTensorAlgEquiv_symm_X, hp, TensorProduct.map_tmul, map_one,
  IsScalarTower.coe_toAlgHom', Generators.algebraMap_apply, aeval_X, e]

Result:
case h_X
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 : MvPolynomial P.vars T
i : P.vars
hp : (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm p) = (aeval P.baseChange.val) p
⊢ (aeval P.baseChange.val) p * 1 ⊗ₜ[R] P.val i = (aeval P.baseChange.val) p * (aeval P.baseChange.val) (X i)