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

Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply,
  TensorProduct.includeRight_apply, TensorProduct.lift_tmul, map_one, mapAlgHom_apply, one_mul]

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✝) = eval₂ (C.comp ↑(ofId R T)) X (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
⊢ RingHom.ker (aeval P.baseChange.val) ≤
    Ideal.span (Set.range fun i => (MvPolynomial.map (algebraMap R T)) (P.relation i))

Tactic:
intro x 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 : x ∈ RingHom.ker (aeval P.baseChange.val)
⊢ x ∈ Ideal.span (Set.range fun i => (MvPolynomial.map (algebraMap R T)) (P.relation 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
⊢ a ⊗ₜ[R] 1 = (aeval P.baseChange.val) (C a)

Tactic:
erw [aeval_C]

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 = (algebraMap T (T ⊗[R] S)) a

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
⊢ (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm x) = (aeval P.baseChange.val) x

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

Tactic:
simp only [SetLike.mem_coe, RingHom.mem_ker, ← Z, ← hy, algebraMap_apply,
  TensorProduct.includeRight_apply]

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

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

Tactic:
apply le_antisymm

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

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

Proof state:
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✝) = eval₂ (C.comp ↑(ofId R T)) X (P.relation x✝)

Tactic:
rfl

Result:
no goals